Anthropic says Claude proved 239 OSS-Fuzz entry points crash-free, down to the compiled binary

Anthropic’s Frontier Red Team, working with the startup Theorem, says Claude wrote machine-checked proofs that 239 OSS-Fuzz entry points across 123 open-source libraries never crash on any input under 64 MB.

What was proved

The proofs are in Rocq and target the compiled RISC-V binary, not the source code. Anthropic puts the total at about 180 million lines of proof, with a typical proof around 600,000 lines and a median binary of 18,000 instructions. Along the way Claude found and patched bugs before proving the fixed code, including a decompressor write past its buffer that needs a 20 MB input and a rediscovery of CVE-2026-56132 in libexpat. Anthropic says one PDF reader yielded as many security bugs in a week as it usually reports in a year.

The fine print

The theorem holds for a single-threaded, statically linked RISC-V binary built against musl, on Linux, with a fixed memory budget. You must trust the RISC-V and Linux models, the theorem statements and the Rocq checker. Anthropic says plainly that formally verified does not mean bug-free: the crash oracle is AddressSanitizer, which misses some memory bugs, not every entry point was covered, and most people run x86 or ARM with glibc. Proofs can take hundreds of millions of tokens.

What you can use

A subset of the proofs and the RISC-V and Linux semantics are public under MIT. Theorem’s OSS Verify offers the pipeline free to qualifying open-source projects, with a Claude skill for adding one. Anthropic also reports a Rust Python interpreter proved with Verus that matched CPython on 99.95% of 1.7 million random programs, and says Opus 5.5 proved half of 36 test tasks with about 40% fewer tokens than Opus 5.

Why it matters

Fuzzing finds crashes it happens to hit. A proof covers every input inside its assumptions. If you maintain an OSS-Fuzz project, the useful question is whether your real build matches those assumptions.