Anthropic and Theorem report Claude proving no-crash properties on 123 open-source libraries

The team turned existing fuzz tests from Google's OSS-Fuzz project into formal specifications over compiled RISC-V binaries, then had Claude write the proofs and a Rocq proof checker validate them. The post reports proofs for 239 entry points in 123 libraries, about 180 million lines of Rocq in total, with a typical proof near 600,000 lines. Where proving failed, Claude patched the bug it found and proved the patched version. The authors say some of those bugs are ones a fuzzer would be unlikely to reach, including a counter underflow that needed inputs of around 20 MB with one rare layout.

The cost figures are the part to read closely. The authors say proofs can take hundreds of millions of tokens. On 36 small tasks, they report Opus 5.5 proving half of them with about 40% fewer tokens than Opus 5, and agents that could copy each other's proofs used 17% fewer tokens than agents working alone.

The limits are stated in the post. The proofs assume a single-threaded static RISC-V binary on Linux, and the authors write that "formally verified" does not mean bug-free, since a proof is only as good as the spec and the machine model. These are first-party results. We read the post body; the appendix was not read and we did not check the published proofs.

Why it matters: If the cost keeps falling, a fuzz test becomes a spec and a proof becomes a check that does not depend on trusting the agent that wrote it. That is a different verification loop from reviewing generated code, and worth watching for anyone deciding what a factory should demand before merge.