Claude proved 123 libraries' fuzz tests never crash
Why it matters
Anthropic's Frontier Red Team, working with Theorem, used Claude to formally verify that 239 fuzz-test entry points across 123 open-source OSS-Fuzz libraries never crash, on any input up to 64 MB. They turned the fuzz tests developers had already written into specs ("this test never crashes") over compiled RISC-V binaries; Claude wrote the proofs, about 180 million lines of Rocq over a few weeks, and the Rocq proof checker checked them. Along the way it found and patched hundreds of bugs, including an out-of-bounds write that only showed up on inputs around 20 MB, which fuzzers would be unlikely to find. In a separate effort on a widely used PDF reader, the team found as many security bugs in one week as are typically reported in a year. It is getting cheaper: Opus 5.5 proved half of 36 test tasks with about 40% fewer tokens than Opus 5, and sharing proofs between agents cut tokens 17%. For context, the seL4 kernel took 2 person-years to build and 20 to verify. Caveat: "formally verified" does not mean bug-free. The proofs assume single-threaded static RISC-V binaries on Linux, while most people run these libraries on x86 or ARM, and proofs can take hundreds of millions of tokens. Anthropic is publishing a subset of the proofs, and Theorem is offering to run the pipeline for other open-source projects.
Read the source: Anthropic (opens in a new tab)
All hits from 23 Oct 2026More SecurityGet the daily hits by email