Claude writes proofs that 239 fuzz tests cannot crash

Anthropic says Claude wrote machine-checked proofs that 239 test entry points across 123 open-source libraries will not crash on any input under 64 MB. The proofs work on compiled RISC-V machine code and are written in the Rocq proof language. Anthropic described the work Thursday with Theorem.

Formal verification means proving that code always follows a set of rules. It has long been rare. Anthropic notes that the seL4 kernel took two person-years to build and 20 person-years to verify. The company says AI models now make that kind of proof practical at scale.

What Claude proved: The team started with fuzz tests from Google’s OSS-Fuzz project. A fuzz test is an entry point that developers write so a testing engine can throw random inputs at their code. Any crash is a bug. Fuzzing can never try every input. So the team turned each test into a formal rule: this test never crashes for any input under 64 MB.

OSS-Fuzz builds C and C++ code with AddressSanitizer, which crashes a program on improper memory access. A no-crash proof therefore covers memory errors that tool catches, plus failed assertions. Over a few weeks, Claude patched the bugs it found and proved the rule for 239 entry points, Anthropic says. The proofs total about 180 million lines of Rocq. A typical proof runs about 600,000 lines. The median binary has 18,000 RISC-V instructions.

What readers still have to trust: Almost none of those lines need human review, Anthropic says, because the Rocq proof checker confirms each proof meets its specification. That leaves three things to trust: Theorem’s formal models of RISC-V and of Linux processes, the exact theorem statements and the Rocq checker itself. A footnote adds the hardware, operating system and OCaml compiler the checker runs on.

The proofs also assume a single-threaded static binary, linked against musl libc, with a fixed memory budget on a RISC-V CPU running Linux. Most people run these libraries on x86 or ARM with glibc, Anthropic says. AddressSanitizer does not catch every memory bug. Not every entry point in each library was proved. “This doesn’t mean these libraries contain no bugs,” the post says.

Bugs along the way: The proof attempts surfaced hundreds of bugs, Anthropic says. One was a counter underflow in a decompressor that caused an out-of-bounds write, but only on inputs around 20 MB with a rare layout. Another was an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory. Claude also rediscovered CVE-2026-56132 in libexpat. Fuzzers typically cap inputs at 1 MB, the company notes.

Because Claude could patch code, it could in theory rewrite a program so it trivially never crashes. Anthropic says it penalized patches and logged and audited them.

Our read: This is a real shift in scale, with careful fine print. Anthropic is not claiming 123 libraries are bug-free. It claims specific test entry points cannot crash, under specific conditions, on a machine model it and Theorem built. That is narrower than the 123-library figure suggests, and the post says so plainly. The strength is the checker. A human does not have to read 180 million lines; Rocq does that. The weak points move into a smaller trusted base. If the RISC-V or Linux models differ from reality, a proof can be right about the model and wrong about the world. The gap to everyday x86 and ARM systems is the biggest one. Still, the bugs are concrete. A 20 MB trigger is something a fuzzer capped at 1 MB would likely miss. Cost is the open question: Anthropic says proofs can take hundreds of millions of tokens.

Cost is falling, Anthropic says: On 36 small tasks, Opus 5.5 proved half with about 40% fewer tokens than Opus 5. Agents sharing a workspace used 17% fewer tokens than agents working alone.

What’s next: Anthropic is publishing a subset of the proofs and the RISC-V and OS semantics. It also plans to publish the specifications it could not prove. Theorem is offering to run the pipeline for other open-source projects and is releasing a Claude skill for developers. Theorem has also laid out a roadmap for verifying the Nix ecosystem, including glibc, OpenSSL and cURL. The authors include Anthropic researcher Nicholas Carlini.

Source: Anthropic