Claude proved 123 libraries crash-free. Here's what still needs checking.

That is real, and it is good news. Memory safety of C libraries is provable at scale now, and the proof companies behind this work are building something every team should use. If you ship a parser or a protocol, put it through them. (Source: Anthropic, LLMs are making formal software verification feasible at a much larger scale, 2026-10-22, and its PDF appendix, verified 2026-10-23. Theorem offers the pipeline free to qualifying open-source projects through OSS Verify, verified 2026-10-23.)

Then read how the spec was written. "The difficulty of obtaining a comprehensive and unambiguous spec is a significant obstacle to verifying software at a larger scale", so the team took "the approach of automatically converting their preexisting compilable test suites into a spec". Their limits section says it plainly: "a proof checker can’t tell you whether your spec matches reality", and “Formally verified” does not mean “bug-free.” The tests were the spec. That is the useful lesson, and it is the subject of our formal verification for AI-generated code guide.

What a proof gives you

TLA+ describes every way a system can behave and states which behaviours are acceptable, for example "there are never two leaders". Its model checker, TLC, explores every state of a finite instance and returns a concrete counterexample when one exists. A prover such as Rocq, Lean or Verus goes further: the property holds for all sizes, relative to the spec and the tool's trusted base. The proofs-at-scale work pushed that from hand-written research artifacts to roughly 180 million machine-written lines.

For concurrency, distributed protocols, memory safety, crypto, compilers and anything quantified over an infinite domain, nothing beats it. We concede that ground completely.

Three limits the proof community names itself

You don't need a sceptic to list the limits. The people who build and teach these tools put them in their own primers:

1. A model checker checks a finite model. TLC explores one finite instance; anything beyond it needs a proof (Reasonable's TLA+ primer).
2. The model is not the implementation. In the same primer's words: "The model is not the implementation … the two can drift apart as the code changes". Proving that code refines its model is possible today for Rust in Verus. Most enterprise services are not written that way. (Source: Reasonable's TLA+ primer, verified 2026-10-04.)
3. Some properties can't be stated as a formula over one behaviour. Hillel Wayne, author of Practical TLA+, lists what that leaves out: reachability, properties over two or more behaviours, statistical properties such as a p95 response time, and robustness to code change. There are workarounds, which his long form, What TLA+ can and can't check, calls "useful hacks, but they're still hacks". (Source: Wayne's post on X, 2026-09-24, and the long form, verified 2026-10-23.)

Cheap proofs move the risk to the spec

A proof shows that the code matches the spec. It never shows that the spec matches what the business meant. As proof search gets cheap, every remaining doubt moves to the spec, and today's measurements say machine-written specs are the weak step:

• Pure Dafny verification of given specs rose from 68% to 96% in a year. Among vericoding successes across Dafny, Verus and Lean, about 9% of the specs were too weak and another 15% poorly translated (Vericoding, arXiv 2509.22908, verified 2026-09-25).
• TLA+ written from natural language came out at best 8.6% semantically correct when checked by TLC, the best prompting strategy's pooled rate across 30 LLMs (arXiv 2606.05792, verified 2026-09-25).
• Leading LLMs average around 41% on the invariants of real-system TLA+ models (SysMoBench's authors, verified 2026-09-25).

Martin Kleppmann, who predicts formal verification goes mainstream, says the same: "the challenge will move to correctly defining the specification" (verified 2026-09-25). In business software, the spec is your requirements, your acceptance tests and your business rules. When tests become the spec, their strength bounds what any proof means. The article's appendix measured it, on a verified interpreter: "we deliberately injected seven bugs … Five survived the random tests, while all seven broke the proof". That is mutation analysis, run on the spec's source.

Business software lives in comparisons

Most of the properties that decide whether a release of business software is safe compare two things:

The industrial record points the same way. AWS's Cedar team found 4 bugs while writing proofs, and 21 more by differential and property-based testing around the verified model (arXiv 2407.01688, verified 2026-09-25). Proof and testing together, each where it is strongest.

What Karate Agent does with the rest

Karate Agent is the governance layer for AI-built software. Requirements, business rules, tests and evidence live in one git-native graph that your agent drives and a human audits. For the questions above:

• The model is executable, and it is the test oracle. Business rules live in a rulebook and lifecycles in a state model. The engine walks every command order under declared ceilings and replays its witnesses against the real service. A refusal given for the wrong reason is its own finding.
• Where the domain is finite, you get the proof-grade answer. A guarantee over a fully enumerated input domain reads proven for this input domain, and a billion-row domain is certified once, so every later check reads proven for this input domain too. Anything less reads sampled, with the cause named. A situation the rules make impossible blocks the release as not reachable, proven for this input domain.
• Meaning drift is caught under a green suite. An output, a decision or a guarantee that moved with no example edited is reported against a blessed baseline, at rule and lifecycle depth.
• The tests themselves are graded. Mutation testing scores whether your assertions would notice a seeded defect, and assertions copied from observed output can't inflate the score. See how →
• Every verdict lands on a requirement. A violated guarantee turns its requirement FAILING and the release NOT READY, with the breaking input attached. When an AI run ticks off a requirement, it reads as an AI claim, graded below captured evidence. AI-authored requirements, rules and tests stay marked review-pending until a human signs off, and the release gate counts what is still unreviewed. Roadmap

The rules engine behind this is business rules testing. Why the gap grows as AI writes more code: AI verification debt.

Bring your proofs

None of this is a reason to skip formal methods. Use them, and connect them to the release:

• Today, TLC on the requirement. A TLC model-checking result lands on the acceptance criterion it argues for. A counterexample fails it, an edited spec or model marks it stale, and a project can block any release missing a proof. A TLC counterexample's steps are saved as a sequence on the lifecycle model and replayed against the running service on every commit: the design bug the model found becomes a regression check on the shipped code, tied to its requirement.
• Proofs on the requirement graph. Roadmap A Rocq, Lean, Verus, Dafny or Alloy result lands on the requirement it argues for, bound to the theorem statement and the code it was about, with the prover's own assumptions report beside it, verbatim. It stops counting when the statement or the code moves.
• Who reviewed the theorem. Roadmap An AI-written theorem statement is unreviewed AI work, and on a high-criticality requirement it blocks release until a human signs it.
• No green bought by refusal. Roadmap A guarantee that turns green because the rules now refuse more input, or because its assertion was rewritten, is reported, never credited. It is the reward hacking the article's authors had to audit by hand: "Claude could make any theorem provable by rewriting the program into one that trivially never crashes".

A proof tells you the code matches the spec. We tell you whether the spec matches the business, and whether your tests would notice when either one moves.

See it on public projects

• TLC beside the running service. In the public fleetquote kit, TLC checks a TLA+ model of the quote lifecycle and finds no error, while the executable twin catches a defect planted in the service code against the running service. TLC flags the same invariant only in a weakened copy of the spec, where a modeller wrote the defect into the model. The TLC runs →
• quick-meetings-karate. The repo takes a published meeting scheduler and the five bugs an InfoQ article seeds into it, and finds the same five with an agent-written rulebook and lifecycle model. Every branch's verification record is published.