Claude found bugs missed by years of testing while writing security proofs, Anthropic says

A mathematical proof can promise more than trillions of software tests—but only within the rules it actually proves. On October 22, 2026, Anthropic and collaborator Theorem reported using Claude to prove security properties for 239 entry points across 123 open-source libraries. The work also uncovered hundreds of bugs, without establishing that those libraries are generally bug-free.

Anthropic says some defects had survived years of testing, despite trillions of test runs. Conventional testing can expose failures by trying enormous numbers of inputs, but cannot guarantee that every possible route through a program has been checked.

Turning existing tests into guarantees

The researchers started with Google’s OSS-Fuzz initiative, which continuously tests qualifying open-source projects. Fuzzing feeds generated and mutated inputs into developer-supplied entry points—routes into the code—looking for crashes.

The team reused those tests as mathematical specifications. It compiled each library and test into RISC-V machine instructions, then asked Claude to prove that the test cannot crash for any input smaller than 64 MB under the modeled conditions.

That can establish more than memory safety. If a compression test crashes whenever compressing and decompressing data fails to return the original input, proving no crashes also proves that round-trip rule.

Claude wrote the proofs; a separate tool, Rocq, checked them against their specifications. Developers do not need to review every generated proof line manually. When bugs blocked progress, Claude could patch the program, regenerate its specification and try again.

Bugs beyond small test inputs

Anthropic says many discoveries would be unlikely to emerge from fuzzing, which typically uses inputs capped at 1 MB. Examples included:

• A decompressor counter underflow that could write outside allowed memory, requiring roughly 20 MB of input in a rare pattern.
• An image-decoder read outside allowed memory that required a 64 MB input and more than 2 GB of memory.

Claude also noticed a non-crashing logic flaw while proving memory safety: a feature restricting which files an application could load was not always enforced.

The guarantee ends at the model’s boundary

The proofs assume single-threaded static binaries, a fixed memory budget and a RISC-V processor running Linux. Their guarantees cover every modeled operating-system response and memory layout—not every real-world environment.

Developers still need confidence in the mathematical models, exact statements being proved and Rocq’s checker. A valid proof cannot protect a behavior its specification never describes.

For outside scrutiny, Anthropic is publishing a subset of proofs and the project’s previously nonpublic trusted components. Theorem is offering to run the pipeline for other open-source projects and publishing a Claude skill to help developers verify their code.