Anthropic reported on October 22, 2026, that Claude and Theorem produced machine-checked no-crash proofs for 239 fuzz-test entry points across 123 Google OSS-Fuzz libraries. The result applies to selected entry points and inputs under 64 MB in a defined RISC-V and Linux model, not to every behavior of each library.
How Claude and Rocq turn fuzz tests into proofs
Fuzzing runs software with many generated inputs to find failures in the executions it tries. Anthropic’s reported process takes existing fuzz tests, turns their expected behavior into a formal specification, then asks Claude to generate proof code for compiled RISC-V binaries. The Rocq kernel checks whether each proof follows from that specification. Theorem supplied the RISC-V instruction and Linux process semantics used in the model.
A checked proof establishes that the modeled program satisfies the stated property. It does not independently establish that the specification captures every behavior people expect from the software.
What the 239 proofs cover
Anthropic says the main theorem concerns whether a selected fuzz-test entry point crashes on any input below 64 MB, including modeled memory-safety errors and failed assertions. The binaries were modeled as single-threaded and static, with a fixed memory budget, on Linux using RISC-V instructions. Their median length was 18,000 RISC-V instructions.
The boundary matters: Anthropic says it did not verify every entry point in each library. A proof for one selected entry point does not cover every library function, caller, or deployment configuration. A deployed program may also use a different architecture or dynamic linking, unlike the main model.
Bugs Anthropic reported during proof attempts
Anthropic says Claude patched bugs it encountered while trying to prove the specified properties, then regenerated the specifications against the patched code. The company says it penalized patches, requested evidence of which inputs they changed, and logged and audited them to reduce the risk of reward hacking.
Reported examples include a decompressor counter underflow that led to an out-of-bounds write on a rare input around 20 MB, and an image-decoder out-of-bounds read that required a 64 MB input and more than 2 GB of memory. Anthropic also reports an out-of-bounds read triggered by a particular sequence of calls across two file handles, and the rediscovery of CVE-2026-56132 in libexpat with deeply nested input.
Why a machine-checked proof is not a bug-free certificate
The guarantee depends on the property, binary, input bound, and machine model specified for the proof. Rocq checks the proof against that formal statement; it does not decide whether the statement captures all real-world behavior. Anthropic also notes that AddressSanitizer, a tool that detects certain memory errors while code runs, misses some memory-safety bugs. Calls from other software and unverified code paths are outside the result’s stated coverage.
What the appendix adds about proof size and Python
Anthropic’s appendix separates roughly one billion Rocq lines generated across proof attempts from about 180 million lines included in proofs that passed checking. A typical completed proof was about 600,000 lines across roughly 1,400 files; checking took 30 minutes to several hours of CPU time. More than half of each proof was machine-emitted by tools Claude wrote, while roughly 40% was proof text.
In a separate Python case study, Verus checked all 17 tiers of a Rust interpreter against the project’s formal semantics. Anthropic separately reports that the interpreter matched CPython’s behavior in 99.95% of more than 1.7 million generated-program comparisons. That percentage comes from empirical testing, not a proof of equivalence for every Python program.
