Anthropic and Theorem used Claude to fix bugs and produce formal proofs for 239 test entry points across 123 open-source libraries in OSS-Fuzz. Anthropic says the work took a few weeks. The proofs establish that selected tests will not crash on any input smaller than 64 MB under specified conditions, rather than merely showing that many samples passed.
Turning fuzz tests into mathematical specifications
The process started with existing fuzz tests, which run code on varied inputs to look for failures. Anthropic converted them into mathematical specifications describing the behavior of compiled RISC-V instructions. The claim to be proved covered every input below the size limit: processing it must not cause the test to crash. Instead of trying more individual samples, Claude was tasked with constructing a proof covering the entire defined input space.
According to Anthropic, the work produced approximately 180 million lines of proofs in Rocq. A typical proof ran to around 600,000 lines, while the verified binaries had a median length of 18,000 RISC-V instructions. To translate machine code into a mathematical model, the project used Theorem’s formal descriptions of RISC-V instructions and Linux processes.
Claude fixed bugs and resumed proving
Attempts to construct proofs uncovered hundreds of bugs, Anthropic says. The researchers designed the process so Claude did not have to wait for a person after each discovery: it could patch the code, have the specification regenerated from the revised version and continue proving that the new specification held.
One example the company describes was a counter underflow in a copy of a decompressor. It caused an out-of-bounds write, but only for inputs of around 20 MB with a rare, particular layout. The researchers say conventional fuzzing would struggle to find it because fuzzers generally mutate small inputs, typically capped at 1 MB.
Proofs can also establish functional properties
According to Anthropic, proving the absence of crashes can also establish a functional property when a test checks it with an assertion. For LZO compression, for example, a test requires compression followed by decompression to reproduce the original input. A violation triggers a crash, so proving that the test never crashes also proves that property.
While verifying cpp-httplib, Claude also had to address the risk of a stack overflow caused by recursion in the std::set destructor, the company says. That recursion depends on the tree’s maximum depth. The work therefore included a machine-code-level proof that the red-black tree rebalancing algorithm in libc++ keeps the tree’s depth logarithmically bounded.
The environment and test coverage define the scope
Anthropic says the proofs cover every modeled Linux response and memory layout. They assume a single-threaded, statically linked program with a fixed memory budget running on a RISC-V processor. The verified binaries use musl libc, whereas common deployments of these libraries also use x86 or ARM processors and dynamic linking with glibc.
Anthropic also notes limits to its coverage of the libraries: it did not verify every entry point, and AddressSanitizer does not detect every memory-safety bug. Even checking all entry points would not necessarily cover dead code, for example. Further bugs can arise in a calling program that misuses a library.
Rocq checks the proofs themselves, so virtually none of the proof code requires manual review, according to Anthropic. Developers must still trust the formal models of the processor and Linux processes. The exact statements of the theorems and the correctness of the Rocq proof checker are equally important.
Opus 5.5 and shared proofs reduced token use in tests
Anthropic also built 36 small verification tasks from OSS-Fuzz code to compare models. In this test, the company says Opus 5.5 completed proofs for half the tasks using approximately 40% fewer tokens than Opus 5.
In another experiment, the company let agents reuse one another’s proofs through a shared workspace. According to Anthropic, they used 17% fewer tokens than when working alone. Some agents also completed tasks they had failed in an earlier solo attempt.
Released proofs and access for other projects
Anthropic is releasing previously unpublished trusted components created for the project, along with complete Rocq proofs for tests that did not require patches. The materials also include specifications for some tests the team could not prove. The company is withholding proofs that could expose an unpatched bug in open-source software.
Theorem is offering to run the same verification process for other open-source projects. It is also publishing a Claude skill designed to help developers get started with verifying their own code.
