Claude writes checked proofs for 239 software tests: What they guarantee

Formal software verification: Technology, limits and analysis

Fuzz testing has made open-source software more robust by throwing enormous numbers of mutated inputs at programs and watching for crashes. But it cannot cover every possible execution path. On October 22, 2026, Anthropic and Theorem introduced a different approach: ask Claude to create formal proofs of properties already captured by existing OSS-Fuzz tests. The result matters because a verified mathematical argument can cover whole classes of possible inputs. That is a stronger kind of assurance than simply running more test cases, provided the theorem and its assumptions accurately match what users need.

The researchers report 239 formally verified fuzz-test entry points in 123 open-source libraries, with approximately 180 million lines of proof code in Rocq. Claude constructed the arguments, while the Rocq proof checker verified whether each argument satisfied its mathematical specification. The team compiled the relevant software and tests into RISC-V instructions and translated their execution into a formal model. This is not proof that every function in each of the 123 libraries is safe: the measured unit is a particular executable test entry point and the behavior that its specification captures.

The conditions are fundamental rather than footnotes. The no-crash properties cover inputs smaller than 64 megabytes, modeled Linux responses and memory layouts, a fixed memory budget, and single-threaded, statically linked binaries on RISC-V. Production software commonly uses other processor architectures, multithreading, dynamic libraries, complex operating-system interfaces and external services. The reported proof does not automatically extend to any of those. The semantics of the CPU and operating system, the precise theorem statement, and the Rocq checker remain trusted components.

Anthropic reports hundreds of bug discoveries during proof attempts and describes letting Claude fix some defects before trying again. One case involved a decompression bug reachable only through a rare structure in an input of roughly 20 megabytes. This illustrates another potential benefit: a proof that fails may expose a real counterexample or defect that ordinary fuzzing missed. Such examples come from the authors' primary research report, however. They should not be presented as an independent audit of every code patch, nor does discovering one category of flaw imply the absence of other security risks.

A cautious engineering workflow would start with a narrowly scoped library and a precisely documented specification. Keep the exact binary, compiler, operating-system model, input limit and hardware semantics together with the proof artifact; run the checker independently. Any proposed fix still needs code review, regression testing and a controlled release process. A no-crash property does not establish authorization correctness, confidentiality, resistance to side channels, or business-rule validity. Those require their own specifications and evidence.

The editorial significance is the move from AI-generated tests toward AI-generated, independently checkable claims about software behavior. The promise is important for maintainers who cannot afford years of formal-methods engineering. Yet generalizing from these proofs to production cloud services, native x86 builds or concurrent systems is still future work. The key question is not how many lines of proof an AI can write, but which real-world property an independently reproducible proof actually guarantees.

Original sources and further reading

• Anthropic – LLMs are making formal software verification feasible at a much larger scale ↗
• Anthropic/Theorem – veröffentlichtes Beweis-Repository ↗

The evidence was reviewed against the cited primary documents; no independent product or lab test was performed.

Explore AI agent security →

Read about AI-assisted PHP flaw discovery →