Claude wrote no-crash proofs for 123 OSS-Fuzz libraries

Anthropic’s Frontier Red Team and Theorem gave Claude a fuzz harness and a compiled RISC-V binary, then had it prove that no input under 64 MB can crash the program. Over a few weeks Claude did this for 239 entry points across 123 OSS-Fuzz libraries. The proofs total about 180 million lines of Rocq, a proof assistant whose kernel checks every step, and almost none of them needs a human to read them.

The work is described in a post on Anthropic’s research blog dated October 22. The team says that, as far as it knows, this is the first large-scale use of AI to formally verify production software at the assembly level. Writing the proofs also turned up hundreds of bugs, some of which had gone unnoticed for years “despite trillions of test runs.”

From fuzz test to theorem

Any verification project starts by defining what “correct” means for the code. For a PNG decoder, RFC 2083 spells out the correct output. A text editor or a browser has nothing like that, and the post names the lack of a full, unambiguous spec as a major obstacle to verifying software at scale.

The team worked around it with tests developers had already written. A fuzz harness is an entry point that accepts arbitrary bytes, and any input that crashes it counts as a bug the authors care about. OSS-Fuzz builds C and C++ projects with AddressSanitizer, which turns improper memory access into a crash, so a harness also catches memory-safety errors. A fuzzer throws huge numbers of mutated inputs at that entry point, but no number of runs is guaranteed to cover every code path.

The pipeline turns the harness into a theorem. The library and its fuzz test are compiled to a RISC-V executable. That binary, Theorem’s formal semantics for RISC-V instructions and Linux processes, and the no-crash property together produce a spec mechanically. The spec says the program exits normally, with no memory-safety error and no failed assertion, for every input under 64 MB and for every OS response and memory layout the model allows. Claude writes the proof and the Rocq kernel checks it. Once that proof goes through, fuzzing the entry point on RISC-V can no longer find anything.

Size is what used to rule this out. The post cites seL4: two person-years to build the kernel, 20 to verify it. Here the 180 million lines are spread across the 239 entry points, and a typical proof runs to about 600,000 lines for a binary with a median of 18,000 RISC-V instructions. The authors argue that grinding through millions of lines toward one well-defined goal is work LLMs are extremely well suited to.

What still has to be trusted

Because Rocq confirms that each proof meets its spec, a developer has to trust only three things: the formal models of RISC-V and Linux processes, the exact theorem statements, and the Rocq checker itself. Those components do not grow as more projects are added, and the authors call hardening them a far more tractable task than debugging every line the proofs cover.

The guarantee has explicit conditions. The program has to run as a single-threaded static binary with a fixed memory budget on a RISC-V CPU under Linux. Bugs can still sit in the trusted components or outside the scope of the proof, and the authors say plainly that this doesn’t mean the libraries contain no bugs. They call broader coverage “well within reach,” since it would involve standardizing semantics for more assembly architectures and other OS processes.

Bugs found along the way

When a proof attempt fails, the failure points at what could break the property. The team didn’t want Claude stopping for a human every time, so it let Claude patch the code itself. The spec was then regenerated from the patched code, and Claude proved the new version.

Many of these bugs, the post says, are ones a fuzzer would be unlikely ever to find. Fuzzers mutate small inputs, typically capped at 1 MB, and usually rely on code coverage to steer them. The proof has to hold on every path reachable from the entry point, for any input up to 64 MB.

Beyond the fuzz-test work, Anthropic describes initial explorations with other verification methods: assessing the security of zlib, proving behavioral equivalence for a Python interpreter written in Rust, and rooting out long-standing bugs in critical software.

What you can pick up

Anthropic is publishing the trusted components that weren’t already public, Claude’s complete Rocq proofs for fuzz tests that needed no patching, and the specs for fuzz tests it could not prove. Theorem is offering to run the same pipeline on other open-source projects and is releasing a Claude skill to help developers start verifying their own code.

The authors expect proof costs to keep falling as models improve and as proofs get reused across codebases. “We encourage all developers to explore formal verification with LLMs—especially those who previously tried it with less capable models and found it didn’t work,” they write.