Anthropic says Claude found and patched bugs, then produced formal proofs for 239 test entry points across 123 open-source libraries. The proofs show that the compiled tests cannot crash for inputs smaller than 64 MB under the conditions the researchers modeled.
The work, done with Theorem, turns fuzz tests into statements that can be proved mathematically. Fuzz tests normally try many generated inputs to find crashes. A proof covers every input within its stated limits, according to Anthropic.
The team used entry points from Google’s OSS-Fuzz initiative. Claude patched bugs it encountered, then worked from specifications regenerated for the patched code. Anthropic says the process uncovered hundreds of bugs, including an out-of-bounds write in a decompressor that required an input of around 20 MB with a rare layout.
Proofs apply to compiled RISC-V instructions
The proofs apply to compiled RISC-V instructions. They cover memory-safety errors and failed assertions for inputs smaller than 64 MB, across modeled Linux responses and memory layouts. They assume a single-threaded static binary with a fixed memory budget running on a RISC-V CPU under Linux. They do not establish that the libraries are free of every kind of bug.
Anthropic says the proofs contain about 180 million lines of Rocq code. A typical proof runs to about 600,000 lines for a binary with a median length of 18,000 RISC-V instructions. Rocq checks whether each proof satisfies its specification.
Anthropic is publishing its semantics and proofs
Anthropic is publishing the RISC-V and operating-system semantics used in the work, complete proofs for fuzz tests that needed no patches, and specifications for some tests it could not prove. Theorem is offering to run the same process for other open-source projects and is publishing a Claude skill to help developers try it.
