Claude proves 239 open-source entry points can't crash

AI has spent October finding holes. Here it's proving their absence.

Anthropic's Frontier Red Team said on Oct. 22 that, working with Theorem, Claude produced formal proofs that 239 fuzz entry points across 123 libraries from Google's OSS-Fuzz project never crash for any input under 64 MB. The proofs are checked by the Rocq proof checker and cover the compiled RISC-V binaries, not the source code.

Anthropic says that, to its knowledge, this is "the first large-scale effort to use AI to apply formal verification to production software at the assembly code level."

How Claude did it

Claude turned existing fuzz tests into specifications, then proved that each compiled entry point never crashes under those specs. When a proof attempt exposed a bug, Claude patched the code, regenerated the spec and proved the new version.

That loop invites reward hacking, and Anthropic says so. It penalized patches that changed the code's behavior and logged and audited every one.

The scale, per Anthropic:

About 180 million lines of Rocq in total, with a typical proof running about 600,000 lines.

The binaries had a median length of 18,000 RISC-V instructions. Proofs can take hundreds of millions of tokens.

The bugs fuzzing didn't find

Anthropic says the proof attempts turned up hundreds of bugs, many unlikely to be caught by fuzzing. Its examples include a counter underflow in a decompressor that caused an out-of-bounds write, triggered only by rare layouts of inputs around 20 MB. Another was an out-of-bounds read in an image decoder that needed a 64 MB input and more than 2 GB of memory. Claude also rediscovered a known libexpat flaw, CVE-2026-56132.

Separately, Anthropic says one week of verification attempts on a PDF reader surfaced as many security bugs as are typically reported in a year.

This lands in a month when AI is finding bugs faster than people can fix them. TopFive's Oct. 22 lead was PHP shipping fixes for AI-found critical flaws. Finding bugs scales with AI. So, it now appears, does proving they're gone.

What "verified" does and doesn't mean

Anthropic is careful here, and you should be too. "Formally verified" does not mean bug-free, it writes. A bug can sit in the spec, or in the model of the machine and operating system the proof assumes.

The assumptions are narrow. The proofs assume a single-threaded static binary with a fixed memory budget on a RISC-V CPU under Linux, built on musl libc. Most real deployments use glibc and dynamic linking. Not every entry point was verified, and the proofs don't cover callers who misuse a library.

The cost is falling, though. On 36 small verification tasks, Anthropic says Claude Opus 5.5 proved half using about 40% fewer tokens than Claude Opus 5.

What you can use now

Anthropic is publishing a subset of the proofs on GitHub, along with the RISC-V and Linux process semantics they rest on. It is holding back proofs that could reveal unpatched bugs.

Theorem is offering to run the same pipeline for other open-source projects, and it's publishing a Claude skill to help developers verify their own code.

If you maintain a library with fuzz tests, you already have the starting material. Ask Theorem. Then watch which projects say yes.