Claude Proves Safety of 123 Libraries at the RISC-V Machine-Code Level

Anthropic and Theorem have published the results of a project in which Claude autonomously wrote formal correctness proofs for real open-source code. The model proved the absence of crashes for 239 entry points in 123 libraries from Google OSS-Fuzz. The proofs work not with source code but with compiled RISC-V instructions, and together they total about 180M lines of Rocq. Work like this used to take years of effort from a small pool of specialists, so it was applied only where an error costs too much, such as in Airbus avionics.

A fuzz test as a ready-made specification

The main problem with formal verification is that you first have to define what "correct" means. A PNG decoder has RFC 2083, but a text editor or a browser has no clear specification. The researchers got around this by taking developers' existing fuzz tests and turning the condition "the test never crashes" into a formal specification. They wrote it on top of a model of how any RISC-V binary runs under Linux.

A fuzzer tries a huge number of semi-random inputs but does not guarantee full coverage. A proof gives exactly that guarantee: if Claude has proved that the test will not crash on any input smaller than 64 MB, then fuzzing that entry point on RISC-V will find nothing more. OSS-Fuzz builds C and C++ programs with AddressSanitizer, so any invalid memory access counts as a crash. As a result, the proved property automatically includes memory safety, the main source of vulnerabilities.

What the project actually produced

The project took several weeks. The success criterion: Claude writes the proof, the Rocq kernel checks it, and a human does not need to read hundreds of thousands of lines. Three things still have to be trusted: the formal models of RISC-V and Linux processes, the exact statements of the theorems, and Rocq itself.

• 123 OSS-Fuzz libraries, 239 entry points
• about 180M lines of Rocq, with a typical proof of about 600 thousand lines
• median binary: 18,000 RISC-V instructions
• guarantee: correct exit with no memory errors or assertion failures on any input up to 64 MB
• assumptions: single-threaded static binary, fixed memory budget, RISC-V and Linux

The authors themselves stress that this does not mean the libraries contain no bugs. Remaining errors may hide in the trusted components or outside the proved property. What shrinks is the verification surface: covering new projects does not require enlarging the trusted base.

Bugs a fuzzer would not have found

When a proof failed to go through, Claude fixed the code, the specification was regenerated, and the model then proved the new version. This turned up hundreds of bugs. A fuzzer almost certainly would have missed many of them, because it mutates small inputs, usually up to 1 MB. Examples:

• a counter underflow in a copy of a decompressor, leading to an out-of-bounds write, only on inputs of about 20 MB with a rare structure
• an out-of-bounds read in an image decoder that needs an input of 64 MB or more and over 2 GB of memory
• an out-of-bounds read in another library after a specific sequence of calls through two descriptors of the same file
• a rediscovery of CVE-2026-56132 in libexpat, which requires deep nesting
• a logic error with no crashes: a function that limits uploaded files did not always work

There is also an important side effect: even a failed proof attempt exposes real defects. In addition, fuzz tests often check high-level properties, such as lossless encode-decode round trips. For the LZO compression algorithm, the test asserts that decompressing compressed data returns the original. If the property is violated, the program crashes, so proving the absence of crashes is equivalent to proving the property itself. For cpp-httplib, Claude had to separately rule out a stack overflow caused by deep recursion in the destructor of std::set.

Practical takeaways for teams

The context for this work is stark: more than 1000 vulnerabilities were recently disclosed in the Linux kernel, and models are getting better at chaining small bugs into exploits. For comparison, implementing the seL4 kernel took two person-years, and verifying it took twenty. If the cost of proofs falls as model capabilities grow, and finished proofs can be reused across codebases, the economics change.

Anthropic is publishing some of the proofs, the RISC-V and OS models, and the specifications for tests it could not prove. Theorem offers to run the same pipeline on other open-source projects and is releasing a Claude skill for self-service verification. Developers who once tried formal methods on weaker models and gave up should revisit the question. A sensible place to start is a project that already has high-quality fuzz tests: the specification there is almost ready. In parallel, the authors are trying the same methods on zlib and on checking behavioral equivalence of a Python interpreter written in Rust.