Anthropic says Claude has mathematically proven that fuzz-tested code in 123 open-source libraries can’t crash on any input under 64MB, and it found bugs along the way that years of testing had missed.
The work, published by Anthropic on October 22 with formal verification startup Theorem, covers 239 entry points from Google’s OSS-Fuzz project. Anthropic calls it the first large-scale effort to use AI to formally verify production software at the assembly code level.
From tests to proofs
Fuzzing throws huge numbers of random inputs at a program to see what breaks, but it can never try every input. Anthropic turned each existing fuzz test into a formal rule, “this test never crashes,” and had Claude prove it holds for every input under 64MB.
The proofs work on compiled RISC-V machine code rather than source code. Over a few weeks, Claude wrote about 180 million lines of proofs in the Rocq proof assistant, around 600,000 lines for a typical program. No human has to read them; the Rocq checker confirms each one mechanically.
Bugs testing missed
Whenever a proof failed, Claude had found a bug, patched it and tried again. Anthropic says the effort turned up hundreds of bugs, including an out-of-bounds write in a decompressor that only appeared on inputs of about 20MB with one rare layout, and a rediscovery of a known flaw in the libexpat XML parser.
In separate tests, Claude proved the Linux kernel’s zlib code matches the format’s specification, and while trying to verify a widely used PDF reader, it found as many security bugs in one week as are typically reported in a year. Details are in the technical appendix.
What it doesn’t prove
Anthropic is explicit that “formally verified” doesn’t mean bug-free. The proofs assume single-threaded, statically linked RISC-V binaries on Linux, while most real deployments run on x86 or ARM. The memory checks used don’t catch every memory-safety bug, and not every entry point in each library was covered.
Cost is the other catch: proofs can take hundreds of millions of tokens. Anthropic says Claude Opus 5.5 solved half of a 36-task benchmark with about 40% fewer tokens than Opus 5, and agents that shared proofs used 17% fewer tokens.
Why it matters
AI is getting very good at finding bugs, as the PHP2Shell flaws showed this week. Proofs are a way to show that whole classes of bugs simply aren’t there. Theorem has released a Claude skill for open-source maintainers who want to enrol their projects, and it estimates that 95% of the machine code in the Nix software ecosystem could be verified by the end of 2027 for about $134 million.
