Anthropic says Claude proved 239 test entry points in 123 open-source libraries never crash

A fuzzer can only say it hasn't found a crash yet, and these proofs rule one out for every input in range.

By Think Facility · October 23, 2026 · Anthropic Cybersecurity

On October 22, 2026, Anthropic published research done with a company called Theorem, in which Claude wrote mathematical proofs that 239 test entry points across 123 open-source libraries can't crash on any input under 64 MB. The proofs cover the compiled machine code itself, and a program called the Rocq kernel checks every line of them.

Anthropic calls it the first large-scale use of AI to formally verify production software at the assembly level. Along the way Claude found and patched hundreds of bugs, some of which years of automated testing had missed.

Libraries: 123 from OSS-Fuzz
Entry points proved: 239
Proof size: about 180 million lines of Rocq
Inputs covered: every input less than 64 MB
Time taken: over the span of a few weeks

What Claude proved

The starting point was fuzz testing. Google's OSS-Fuzz service runs these tests continuously for qualifying open-source projects. A fuzzer can run for years and still miss a path through the code, because there's always another input it hasn't tried.

Anthropic and Theorem turned each existing fuzz test into a formal rule: this test never crashes, for any input under 64 MB. Then they asked Claude to prove it over the compiled RISC-V binary, a chip design like x86 or ARM. When the proof got stuck on a real bug, Claude patched the code and proved the patched version instead.

A typical proof runs to about 600,000 lines, for a binary with a median of 18,000 instructions. Nobody reads those lines. What has to be trusted is much smaller: Theorem's models of the chip and of Linux, the exact statements proved, and the Rocq checker. Anthropic is publishing the pieces of that which weren't already public, plus the proofs for tests that needed no patch.

While writing the proofs, Claude also discovered bugs that had eluded detection for years, despite trillions of test runs .

From LLMs are making formal software verification feasible at a much larger scale \ Anthropic

The bugs fuzzing missed

Fuzzers usually cap their inputs at 1 MB, Anthropic says, and some of these bugs only appear far past that. One was a counter underflow in a library's copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB with one rare layout. Another, in an image decoder, needed a 64 MB input and over 2 GB of memory.

Claude also rediscovered CVE-2026-56132 in libexpat, a bug that needed deeply nested input. It found logic bugs that never crash, too: in one library, a feature meant to restrict which files an app can load wasn't always enforced. Outside the fuzz work, an attempt to verify a widely used PDF reader turned up as many security bugs in one week as usually get reported in a year.

Anthropic doesn't name the libraries behind most of these bugs, and it's holding back any proof that might reveal one that's still unpatched.

Where the proofs stop

Anthropic is plain about the limits. The proofs assume a single-threaded static RISC-V binary linked against musl libc, while most people run these libraries on x86 or ARM with glibc. The memory checker that makes bad memory access crash doesn't catch every memory bug, and not every entry point in each library was proved.

“Formally verified” does not mean “bug-free.”

LLMs are making formal software verification feasible at a much larger scale \ Anthropic

Cost is the other limit, since one proof can take hundreds of millions of tokens. On 36 small verification tasks built from OSS-Fuzz code, Anthropic says Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. Agents that could copy each other's finished proofs needed 17% fewer tokens than agents working alone.

I'd treat the 40% as a first reading: the tasks are Anthropic's own, and each got three attempts at a 5 million token budget. Theorem's eval points the same way. Across seven Anthropic and OpenAI models released between May and September 2026, it measured verification speed doubling about every two months.

What it means for the software everyone runs

Google started OSS-Fuzz in 2016 because of Heartbleed, a simple buffer overflow in OpenSSL that, in Google's words, had the potential to affect almost every internet user. As of August 2023, OSS-Fuzz had helped fix over 10,000 vulnerabilities and 36,000 bugs across 1,000 projects. Fuzzing is how a lot of the internet's shared plumbing gets its memory bugs caught.

A proof changes the promise. A fuzzer says it hasn't found a crash yet. A proof says no input in range can cause one, given the assumptions above. Earlier this week Claude went after the same kind of code from a different angle, cutting the parts an attacker can reach (our story).

Theorem has put a price on the bigger goal. In a September 29, 2026 post, it estimates that 95% of the machine code in nixpkgs, a package collection that includes glibc, OpenSSL and curl, could be verified by the end of 2027 for about $134 million, if models keep improving at verification as fast as they have. For scale, it cites a GovAI estimate of about $500 billion a year in global cybercrime damages. That timeline rests on the two-month doubling holding, and the sources don't settle whether it will.

For the people who maintain these libraries, the offer is already open. Theorem runs the same pipeline free for qualifying open-source projects through a program it calls OSS Verify, enrolled by pull request the way OSS-Fuzz is. Its FAQ is direct about who writes the fixes.

Findings and patches are generated by AI models, and we don’t promise that a person reviews them before we send them.

From OSS Verify | Theorem

Only a project's core maintainers can enroll it, and Theorem says it will put widely used critical infrastructure first.