Anthropic and formal-verification company Theorem used Claude to generate roughly 180 million lines of mathematical proof code for test programs drawn from 123 open-source libraries in Google’s OSS-Fuzz project.
The system translated crash tests into formal problems, analyzed compiled machine code and produced proofs checked by Rocq, an independent proof verifier. Anthropic describes the generation process as largely autonomous, although people built the surrounding tools and mathematical foundations. While attempting proofs, the model also found hundreds of bugs that conventional testing had missed, including faults triggered only by unusual input sizes or access sequences.
Formal verification provides a stronger guarantee than ordinary tests, but only inside a precise model. These proofs assume a specified processor architecture, single-threaded execution and inputs below 64 MB. They do not establish that every build or real-world deployment is error-free. The compute burden is also substantial: individual proofs can use hundreds of millions of tokens, and Anthropic did not disclose the project’s total cost.
The work suggests AI could make formal methods practical for more software, especially when a machine checker can reject invalid proof steps. The immediate result is narrower: defined portions of existing libraries were verified under constrained conditions, with reusable proofs and bug reports produced along the way.