Claude proved 123 libraries never crash: formal verification with AI

Formal verification is a mathematical proof that a program meets its specification on every allowed input, not only on the inputs someone managed to test. The problem was always cost: experts wrote the proofs, and such projects took years. Anthropic and Theorem tested whether a model could do this work.

They took libraries from OSS-Fuzz, Google's project where popular open-source libraries are fuzzed around the clock and already have fuzzing entry points. These were compiled into static RISC-V binaries linked against musl libc, with a median size of about 18,000 machine instructions. For each entry point they stated a theorem: the program never crashes on any input under 64 MB, for every modelled Linux response and memory layout. A "crash" means a memory error as AddressSanitizer defines it, or a failed assertion.

Claude writes the proof, and the kernel of Rocq checks it. Rocq is the proof assistant formerly known as Coq. This is the key detail: nobody has to take the model's word for anything. If a proof contains a mistake, Rocq simply rejects it, however convincing it looks. Over a few weeks this produced about 180 million lines of Rocq proofs.

Some summaries of the research claim that "Verus for Rust was mainly used". That is not the case. Verus verifies Rust source code and cannot check machine code. The headline result on 123 libraries was obtained on RISC-V with proofs in Rocq.

Verus does appear, but in a separate case study: Claude wrote a Python interpreter in Rust and used Verus to prove it follows the CPython semantics described in an academic paper. On 1.7 million random programs its behaviour matched CPython in 99.95% of tests. x86 appears in another case: Claude directly proved that the x86-compiled zlib in the Linux kernel implements the RFC 1950 standard, using formal x86 semantics that Claude generated itself and tested heavily.

A proof about C source relies on assumptions: that the compiler built exactly what was written and that undefined behaviour plays out predictably. A proof about the binary needs neither. It speaks about the instructions the processor will actually execute, so a compiler bug or a surprising optimisation is already accounted for.

The price is volume. Machine code is much longer than source, and so is the proof: a typical one runs to about 600,000 lines of Rocq. No human would write that. A model can, which is exactly why the approach has only now become realistic.

Attempts to prove the specs uncovered hundreds of bugs. When a proof does not go through, the cause is often a real defect. Claude then patched it, the spec was regenerated from the patched code and the proof continued. Findings include counter underflow, out-of-bounds reads and writes, a rediscovery of CVE-2026-56132 in libexpat that needed deeply nested input, and a logic bug in which a file-loading restriction was not always enforced. One bug had been latent for more than a decade.

Fuzzers rarely find some of these bugs. Some need an input of about 20 or 64 MB, others more than 2 GB of memory or a specific call sequence. This is the core difference between proof and testing: a test checks examples, a proof covers the whole input set within the stated bounds. In a separate study of a PDF reader, a week of work found as many security bugs as are typically reported in a year.

A separate risk is gaming the task. Claude could make any theorem provable by rewriting the program into one that trivially never crashes. To prevent this, any patch was penalised, extra credit was given for proving which inputs a patch changes and how few they are, and all patches were logged and audited. This is the same class of problem as in alignment analyses: the model optimises a formal criterion, and the harness has to make sure it does not satisfy the letter while dodging the point.

The classic illustration of cost is the seL4 microkernel, the first OS kernel with a complete machine-checked correctness proof (2009). The kernel itself, about 8,700 lines of C and 600 of assembly, took about 2.2 person-years. The proof took about 200,000 lines of Isabelle and about 20 person-years including tools and research, of which about 11 went to the seL4-specific proof. Anthropic rounds this to "two years for the kernel, twenty for the proof".

The shift was predicted. In December 2025 Martin Kleppmann, author of Designing Data-Intensive Applications, wrote that AI would make formal verification mainstream. His argument: the main barrier is the cost of proofs, and proofs have a unique property — the checker rejects plausible but wrong reasoning. So the work can be handed to a model that sometimes errs, while trust rests with the checker. Anthropic's publication is the first large confirmation of that forecast on real code.

It is still expensive: one proof can take hundreds of millions of tokens. But the trend is clear. On a 36-task benchmark built from OSS-Fuzz code, Claude Opus 5.5 proves half the tasks with about 40% fewer tokens than Opus 5. When several agents share a proof workspace and reuse each other's lemmas, they need 17% fewer tokens, and two of the proofs could not be completed by agents working alone at all.

The authors say it outright: "formally verified" does not mean "bug-free". A proof is only as good as the layers beneath it. You have to trust the theorem statement, Theorem's RISC-V and Linux process semantics, the Rocq kernel, and beneath it the OCaml compiler, operating system and hardware. If the real machine does something the model does not describe, the proof will not notice.

The claim itself has limits too. The proofs cover single-threaded static RISC-V binaries with musl, while most people run these libraries on x86 or ARM with glibc and dynamic linking. AddressSanitizer does not catch every memory bug. Specific entry points are proven, not the whole library. A caller that misuses the library can still corrupt memory; closing that gap needs per-function obligations on callers, in other words preconditions.

The most interesting takeaway for an everyday developer is not about RISC-V but about how to write code. Back in 1992 Bertrand Meyer described Design by Contract: a function has preconditions (what the caller must guarantee), postconditions (what the function guarantees) and invariants (what stays true throughout). Meyer built contracts into the Eiffel language. Later came Dafny, whose verifier checks code as you type, and Verus for Rust.

A contract is a specification that can be proven. When invariants are written explicitly and formally, the model's job changes: instead of "check that the code is right" it gets a precise statement to prove or refute, and a checker confirms the result. The more formal the contract, the closer the model's reasoning gets to a real proof. Here is what a contract looks like in Verus:

The three ensures lines are postconditions. Verus proves them for every possible pair a and b, not for a dozen examples from a test. Write a <= b instead of a >= b by mistake and the function returns the smaller number; the check fails and points at the violated condition.

An important caveat to the popular claim that "code is no longer tested, it is proven". Anthropic does not say that. The entry points came from fuzz harnesses, a "crash" is defined through AddressSanitizer, and the model heavily tested its own x86 semantics. A model reasoning about invariants without a checker is not a proof but plausible argument that can be wrong. The strength of the approach is the pairing: the model writes, the machine checks. Tests are still needed, because the specification itself can be wrong.

Theorem has opened an oss-verify service: free for qualifying open-source projects, it needs static riscv64 binaries and proves the absence of crashes on any input up to 64 MiB. A run can take several days. The publication's proofs, the RISC-V and Linux process semantics and a Claude skill that helps add your own project are on GitHub. For your own code the barrier is lower than it seems: Verus and Dafny run locally, and you can write contracts and their proofs together with Claude Opus 5.5 through the Kumo API.