Claude Turned 239 Fuzz Tests Into Proofs: 123 Open-Source Libraries Proven Not to Crash on Any Input Under 64 MB at the RISC-V Binary Level, in About 180 Million Lines of Rocq

Anthropic's Frontier Red Team reported on October 22 that, working with formal verification company Theorem, it had Claude automatically turn fuzz tests from Google's OSS-Fuzz into specifications and then write proofs for them. Across 239 test entry points in 123 open-source libraries, Claude proved that the RISC-V-compiled binaries never crash or trigger memory-safety errors on any input smaller than 64 MB. The proofs total about 180 million lines of Rocq, roughly 600,000 lines each, and are checked mechanically by the Rocq proof checker. Along the way Claude found and patched hundreds of bugs, including an out-of-bounds write that only appears on a specific input of about 20 MB, and rediscovered CVE-2026-56132 in libexpat. The proofs assume single-threaded static binaries, a fixed memory budget and RISC-V plus Linux models, so the x86/ARM and glibc setups most people actually run are not covered. A single proof can take hundreds of millions of tokens; on 36 small tasks Opus 5.5 used about 40% fewer tokens than Opus 5.

From "the longer it runs, the safer we feel" to "once it's proven, stop running it"

Fuzzing pours huge numbers of random inputs into a test entry point to see which one crashes the program. The longer it runs, the more bugs it finds, but it can never be exhaustive. Research published by Anthropic's Frontier Red Team on October 22 takes a different route: it treats the entry points developers already wrote for OSS-Fuzz as specifications, namely "this entry point never crashes on any input smaller than 64 MB", and asks Claude to prove that.

The proofs target the compiled RISC-V instructions, not the source code. Partner Theorem supplied formal semantics for RISC-V instructions and Linux processes, Claude wrote the proofs, and the Rocq proof checker verified them. Within a few weeks Claude had finished proofs for 239 entry points across 123 libraries: about 180 million lines of Rocq in total, around 600,000 lines for a typical proof, covering binaries with a median of about 18,000 instructions. Proofs that large don't need line-by-line human review. The only things to trust are the RISC-V and Linux models, the theorem statements themselves and the Rocq checker.

Bugs dug up along the way

Where a proof gets stuck there is often a bug, and Claude was allowed to patch the code and keep going, so it turned up hundreds of problems. Some are bugs fuzzing almost never reaches: a counter underflow in a copy of a decompressor caused an out-of-bounds write that only fires on an unusually laid-out input of about 20 MB, while fuzzers usually cap inputs at 1 MB; an out-of-bounds read in an image decoder needed a 64 MB input and more than 2 GB of memory; and Claude rediscovered CVE-2026-56132 in libexpat. To stop Claude from gaming the proof by rewriting a program into one that does nothing and therefore never crashes, the team penalized patches and audited each one.

The limits are spelled out

The post lists its own limitations. The proofs assume a single-threaded static binary linked against musl and running on RISC-V, while most people run x86 or ARM with dynamically linked glibc; AddressSanitizer itself doesn't catch every memory error, and not every entry point of each library was covered. Cost is another barrier, since a proof can consume hundreds of millions of tokens. Anthropic points to two signs it is falling: on 36 small verification tasks, Opus 5.5 needed about 40% fewer tokens than Opus 5 to prove half of them, and letting agents share a workspace and reuse each other's proofs cut tokens by another 17%.

The proofs that didn't require patches, along with the RISC-V and OS semantics, are public; proofs that could reveal unpatched bugs are being held back. Theorem says it is willing to run the same pipeline for other open-source projects. For teams maintaining low-level libraries, the realistic use may not be "prove everything" but treating it first as a way to find the bugs fuzzers miss.

via: Anthropic: LLMs are making formal software verification feasible at a much larger scale