Anthropic Says Claude Found Bugs That Survived Trillions of Tests by Trying to Prove the Code Was Safe

Somewhere in an open-source decompressor sat a counter that could underflow and write past the end of its memory, but only if you fed it an input of around 20 MB with one rare, specific layout. Fuzzers, which typically cap inputs at 1 MB, were never going to hit it. Anthropic says Claude found it by trying to prove there were no bugs at all.

That is the pitch behind a research post Anthropic published on October 22 with the formal verification startup Theorem. The company says Claude wrote machine-checked proofs that 239 fuzz test entry points across 123 libraries in Google's OSS-Fuzz programme will never crash on any input under 64 MB. Anthropic puts the output at about 180 million lines of Rocq proof, produced over "the span of a few weeks." Along the way, it says, the process surfaced hundreds of bugs, some of which had "eluded detection for years, despite trillions of test runs."

If that holds up, it matters. Formal verification has always been the gold standard nobody could afford. Anthropic's own example is the seL4 kernel, which took two person-years to build and 20 to prove.

The bug haul is the most concrete part of the story. Anthropic lists an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory and a rediscovery of CVE-2026-56132 in libexpat. The more striking claim sits elsewhere: during an attempt to verify a widely used PDF reader, the team says it "found as many security bugs in one week as are typically reported in a year."

The guarantee covers a build almost nobody ships

Now the fine print. These proofs are about single-threaded, static binaries compiled for RISC-V and linked against musl libc. Anthropic says so itself, and adds that "most people run these libraries on x86 or ARM and dynamically link them against glibc."

"This doesn't mean these libraries contain no bugs." Anthropic Frontier Red Team

The company is admirably blunt that "formally verified" does not mean bug-free. The proofs only hold if Theorem's models of RISC-V and Linux processes are right, if the theorem statements say what people think they say, and if the Rocq checker itself is sound. AddressSanitizer, the tool that defines what counts as a memory crash here, doesn't catch every memory bug, and Anthropic did not verify every entry point in each library.

There is a quieter gap too. Curtis Pyke at Kingy AI, who read through the released proofs, points out that none of the public proofs establish termination. A parser stuck in an infinite loop could pass. Pyke also notes that the public release covers 60 entry points across 25 libraries, a fraction of the 239 headline figure. Anthropic says it is withholding proofs that could expose unpatched bugs, which is reasonable, but it means outsiders can check only part of the claim. Pyke's verdict is that "verified" is "too broad to function as a useful procurement requirement on its own."

Then there is the cheat code problem. Because Claude was allowed to patch the bugs it found, it could in principle make any theorem provable by rewriting a program into one that trivially never crashes. Anthropic acknowledges this reward hacking risk in a footnote and says it penalised patches and audited them. Maintainers will still want to check those patches themselves before anything goes upstream.

"Formal verification ... will soon be as practical as fuzzing is today for almost all production software." Anthropic Frontier Red Team

That is a prediction, not a result, and it comes from a company that sells the model doing the proving. Proofs still burn hundreds of millions of tokens. Still, this lands in a year when AI is finding flaws faster than humans can patch them, as Claude Mythos showed with Microsoft. A machine that can prove the fixes hold, even on a narrow slice of hardware, is the more interesting half of that race. The proofs are public. Now somebody independent needs to run them.