Claude proved 123 libraries cannot crash
Anthropic and Theorem had Claude write mathematical proofs that 123 widely used open-source libraries can never crash on any input up to 64 MB. A separate program checked every proof, and the attempt turned up hundreds of real bugs.
ContextFormal verification means proving, not testing, that code behaves as specified. It was so expensive that it was kept for a few critical systems.
Each project already had a fuzz test: a small program that feeds the library random inputs and watches for crashes. Theorem turns that test into a precise claim about the compiled program, a RISC-V binary: no memory errors and no failed assertions for any input under 64 MB. Claude then writes a proof in Rocq, and the Rocq checker accepts or rejects it.
When a proof would not close because the code really could crash, Claude patched the code and proved the new version. That is how the work found hundreds of bugs. The team penalised and audited patches, because an agent could also make a proof pass by rewriting the code to do nothing.
Across 239 entry points in 123 libraries the proofs add up to about 180 million lines, roughly 600,000 for a typical one, and some took hundreds of millions of tokens. Every number here comes from the authors. The proofs, the machine model and the Claude skill used to add projects are public.
123libraries proved crash-free (authors' figure)
Technical details
The guarantee holds for a single-threaded static binary with a fixed memory budget, linked against musl libc, on RISC-V under modelled Linux. Most users run x86 or ARM with glibc, so the proof does not transfer one to one. The authors also note that the crash detector (ASan-class errors) misses some memory bugs, that not every entry point was verified, and that callers can still misuse a library.
On 36 small proof tasks with a 5M token budget per agent, Opus 5.5 finished half of them with about 40% fewer tokens than Opus 5. Letting agents copy each other's proofs in a shared workspace cut tokens by 17%, and solo runs cost more in 30 of 34 completed proofs.
A second case: Claude wrote a Python interpreter in Rust and proved it against a published model of CPython's semantics with Verus. On 1.7 million random programs it matched CPython 99.95% of the time; the authors call the rest known corner cases. Proofs that would reveal unpatched bugs are withheld.
Why it mattersAgents now write more code than people can review, and this is the strongest sign yet that machines can check what machines write. A fuzz test you already have is the starting point, so the cost of entry is lower than it sounds.
For youYour C++ plugin code will not get a RISC-V proof soon, but the habit transfers today: treat each fuzz or property test as a spec and ask Claude to state it precisely. The shared proof workspace result (17% fewer tokens) is a pattern worth copying in your subagent teams.
- Formal verification
- Proving with mathematical logic that a program meets a precise description, for every possible input.
- fuzz test
- A test that throws large amounts of random input at code to find crashes.
- RISC-V
- An open processor instruction set; here, the machine the compiled libraries were proved against.
- Rocq
- A proof assistant (formerly called Coq) whose small checker verifies every step of a proof.
- entry points
- The functions a fuzz test calls into; each one got its own proof.
Sources Anthropic research postReleased proofsRISC-V and Linux semanticsClaude skill for adding projects
