Claude proved 123 OSS libraries crash-free. Read the assumptions before you read the headline
On October 22, 2026, Anthropic's Frontier Red Team, working with Theorem, published results from using Claude to formally verify 239 fuzz-test entry points across 123 open-source libraries. Over a few weeks they converted OSS-Fuzz targets into specifications about the compiled RISC-V binaries, then had Claude write machine-checked Rocq proofs that those binaries never crash on any input under 64 MB. Along the way, Claude found and patched hundreds of bugs.
For anyone shipping C or C++, this moves formal verification from "twenty person-years" to "an agent pipeline and a token budget". But a proof is only as strong as its theorem statement and its machine model, and both have edges.
What actually shipped
From Anthropic's post, the scope is 123 libraries and 239 entry points, all taken from Google's OSS-Fuzz. The proofs are about the compiled RISC-V binaries, not the source. The median binary is 18,000 instructions, and the semantics come from Theorem's formal model of RISC-V and Linux processes. In total there are about 180 million lines of Rocq, roughly 600,000 lines for a typical proof, all machine-checked.
The property is that the entry point never crashes, meaning no memory-safety error and no failed assertion, for any input under 64 MB. It exits normally for every modeled OS response and memory layout. Theorem's repo states the same property as "halts" (exit status 0 or 2, with no crash, hang or sanitizer failure) plus "agrees" (plain and sanitizer builds behave identically). The trusted base is the RISC-V and Linux process models, the exact theorem statements, and the Rocq checker; a footnote adds the hardware, OS and OCaml compiler Rocq runs on.
The bug examples show what fuzzing misses. One was a counter underflow in a decompressor that led to an out-of-bounds write, triggered only by inputs of about 20 MB with one rare layout. Another was an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory. A third out-of-bounds read needed a specific sequence of calls across two handles to the same file. Claude also rediscovered CVE-2026-56132 in libexpat, which needed deeply nested input. And one was a logic bug, not a crash: a feature restricting which files an application can load was not always enforced.
Theorem has released a subset of the proofs, the RISC-V/Linux semantics, and an enrollment repo (theorem-labs/oss-verify, Apache-2.0) that comes with a Claude skill for adding projects. Proofs that could reveal unpatched bugs were held back.
Numbers that matter
| Metric | Value |
|---|---|
| Libraries / entry points | 123 / 239 |
| Total Rocq | ~180M lines |
| Typical proof | ~600k lines |
| Median binary | 18k RISC-V instructions |
| Input bound | under 64 MB |
| Opus 5.5 vs Opus 5, 36 small tasks | half proved, ~40% fewer tokens |
| Shared proof workspace | 17% fewer tokens |
| seL4, for scale | ~2 person-years to build, ~20 to verify |
Illustrative sizing. Anthropic says proofs "can take hundreds of millions of tokens". Assume 300M tokens per entry point. That number is my placeholder, not theirs. At that rate, 239 entry points come to about 72 billion tokens. Even at a blended $5 per million tokens, that is roughly $360k for the whole campaign, or about $1.5k per entry point. That is within reach of an OSS foundation or a vendor's security budget.
This is a much better guarantee than "fuzzed for N CPU-years", and a much narrower one than "memory-safe".
What the guarantee excludes
Anthropic's own words: "'Formally verified' does not mean 'bug-free.'" Theorem's what-gets-proven.md is unusually candid about the gaps.
Threads come first. The model runs one thread, so any program that spawns a thread falls outside it, and data races, the worst class of C++ bug, are simply not in scope. Then there is your build: proofs cover static riscv64 builds against musl, while production usually runs x86-64 or ARM with dynamic glibc. Other compilers, flags and architectures, OSS-Fuzz's x86-64 builds included, are explicitly not covered. The C library, compiler runtime and sanitizer runtime are not instrumented.
Inputs of 64 MiB or more are refused and fall outside every statement. Anthropic says raising the bound is trivial: change the parameter, regenerate the spec, reprove. Until that happens, note that the image-decoder bug above sat at exactly the edge of the bound.
Some things sanitizers can't see are also out. Leaks are off, there is no MemorySanitizer build so uninitialized reads aren't caught, and the vptr check and unsigned overflow are not checked. Neither is an access through another live object. On the caller side, the entry point is verified, but your code calling the library with a dangling buffer isn't, and dead code isn't verified at all. Finally, logic: "never crashes" says nothing about correctness unless the fuzz target abort()s on a violated property. The file-restriction bug was found despite this, not because of it.
Anthropic also describes reward hacking. Claude could make a theorem provable by rewriting the code, so patches were penalized, logged and audited. If you run this yourself, treat AI-generated patches as untrusted. Theorem's repo says the same.
My read: this is a much better guarantee than "fuzzed for N CPU-years", and a much narrower one than "memory-safe". As with verification becoming the bottleneck, the scarce resource is now writing the theorem you actually mean.
What I'd do
First, I'd inventory my C/C++ dependencies against the published list and pin to versions that include the patches; proven-and-patched beats proven-on-paper. Second, I'd read the theorem statement before trusting the badge, checking whether the dependency spawns threads, how big my inputs get, and which architecture I ship on. Third, I'd improve fuzz targets now. The pipeline proves what the target asserts, so a target that calls abort() on violated invariants becomes a functional spec for free.
If you maintain an OSS project with fuzz targets, enroll. You need an OSI license, a public repo, reproducible builds and a security contact. And don't drop ASan, fuzzing or x86 CI: they cover exactly the architecture, threading and libc gaps the proofs leave open.
What I couldn't verify
There is no independent audit of the 180M lines. The proofs are machine-checked, but only a subset is public, so I can't confirm that every claimed entry point has a released proof. The model gap is unquantified: Theorem says its Linux model is "narrower than Linux in places" without listing where. On cost, no dollar or token totals are given per library, so my sizing above is illustrative. I did not independently check the CVE-2026-56132 record.
I'll revisit when x86-64/glibc semantics or threads land in the model.
Sources
Primary: Anthropic, LLMs are making formal software verification feasible at a much larger scale; Theorem, oss-verify (enrollment repo); Theorem, oss-verify: what gets proven.