Anthropic published a research post on October 22, 2026 describing work with Theorem, in which Claude wrote formal proofs that 239 fuzz entry points across 123 open-source libraries can never crash. The proofs target compiled RISC-V binaries rather than source code, and a checker called Rocq validated each one.
What was actually released
The post carries the Frontier Red Team byline and ships artifacts, not just claims: the RISC-V and Linux process semantics built for the project, Claude’s proofs for the fuzz tests that needed no patching, and the specifications for the fuzz tests it could not prove. Anthropic says any proof that might expose an unpatched bug stays unpublished.
The method matters more than the count. Each library in Google’s OSS-Fuzz program ships a fuzz test, a function that crashes when its input breaks something, instrumented with AddressSanitizer. Anthropic compiled those programs to RISC-V, turned each fuzz test into a specification saying the program never crashes for any input under 64 MB, and had Claude write the proof. The Rocq kernel then checks the proof, so virtually none of that code needs a human reader.
| Measure | Figure published by Anthropic |
|---|---|
| Open-source libraries | 123 |
| Fuzz entry points proved | 239 |
| Generated proof code | about 180 million lines of Rocq |
| Typical single proof | about 600,000 lines |
| Median binary under proof | 18,000 RISC-V instructions |
| Largest input covered | 64 MB |
What you can check today
- A subset of the proofs, published so anyone can re-check or reuse them, plus the RISC-V and Linux semantics they depend on.
- The specifications for the fuzz tests Claude could not prove, which mark where the method stopped.
- Theorem offers to run the same pipeline on other open-source projects and publishes a Claude skill to start on your own code.
Claude also fixed what it found, and the bug list is what a security engineer reads first. A counter underflow produced an out-of-bounds write, but only on inputs around 20 MB with one rare memory layout. Another library had an out-of-bounds read that needed a 64 MB input and more than 2 GB of memory. Claude also rediscovered CVE-2026-56132 in libexpat, and found a bug that never crashes at all: a file-loading restriction that is not always enforced.
Two side experiments follow. Claude wrote a formal specification of RFC 1950 and proved that the zlib implementation in the Linux kernel follows it, this time on x86 binaries, then repeated that on half a dozen libraries. It also built a Python interpreter in Rust and proved it against CPython’s semantics with Verus: across 1.7 million random programs, 99.95% behaved identically.
Formally verified does not mean bug-free.
What the claim rests on
That sentence is Anthropic’s own, and it carries the weight of the caveats. A proof is only as good as its model of the machine, and the model here is narrow: a single-threaded static binary, linked against musl, with a fixed memory budget, on a RISC-V CPU running Linux. These libraries ship mostly on x86 or ARM, dynamically linked against glibc, inside threaded applications.
| Assumption inside the proof | What deployment usually looks like |
|---|---|
| RISC-V CPU | x86 or ARM |
| Static, single-threaded binary | threads, dynamic linking |
| musl libc | glibc |
| Inputs under 64 MB | no cap |
| AddressSanitizer-detectable errors | bugs outside what ASan catches |
Coverage has its own edges. Anthropic says it did not verify every entry point of every library, that dead code escapes the proof, and that a caller can still corrupt memory by misusing a verified function.
Then comes the trusted base. The Rocq kernel checks the proof, but it assumes the RISC-V and Linux semantics are correct, that the theorem says what the authors meant, and that the compiler, operating system and hardware under Rocq behave. Those components are published for others to attack, which is the strongest part of the release.
What is not published
No token bill, no dollar cost, no count of entry points attempted against entry points proved, no exact bug count beyond “hundreds”, and no list of the libraries that did not get a proof.
The method has one trap that Anthropic flags itself: a model asked to prove a program safe can rewrite the program into one that cannot crash. Anthropic penalized patches, gave extra credit for proving which inputs a patch changes, and audited the patches afterward.
Cost has to be rebuilt from published prices. The post says individual proofs can consume hundreds of millions of tokens. At the Opus 5.5 rates we recorded from Anthropic’s rate card on October 8, 2026, $4 per million input tokens and $20 per million output tokens, one proof at 100 million output tokens comes to $2,000 before any retry. That is our arithmetic, not a disclosed figure. The trend line matters more: on 36 small tasks, Opus 5.5 proved half with about 40% fewer tokens than Opus 5, and agents sharing a proof workspace needed 17% fewer than agents working alone.
On this page
What it changes for developers who ship AI code
The bottleneck in shipping AI-written code is review, and review is attention that does not scale. This release attacks that bottleneck at one point: a machine-checked proof replaces human attention on the code it covers, without anyone reading 600,000 lines.
It pays first for components that take untrusted bytes: parsers, decompressors, image decoders, which is where the bugs above appeared. The boundary is just as practical: on x86 with glibc and threads, today’s proofs describe a machine you do not run. The guarantee transfers to static binaries and pinned dependencies, not to a typical web service.
For a small team the entry point is not writing proofs. Theorem publishes a Claude skill that walks a developer through the pipeline and offers to run it on other projects, which turns a research result into something with a price.
The Neural Minute take
We covered the other half of this story on October 10, when OpenAI published 372 mathematical results with 42% of the top-line proofs machine-checked in Lean. OpenAI sold results, and the proofs were the receipts. Anthropic sells a workflow applied to code that already ships, and the proofs are the product.
That changes what to ask. In mathematics the specification is the mathematics, so a checked proof closes the question. Here the specification is a fuzz test rewritten as a property, and everything the proof cannot say lives in that rewrite: which entry points, which input size, which machine. If the assumptions match your deployment, a proof beats another year of fuzzing; if they do not, it is a strong hint about a codebase, not a guarantee about yours.
What I would want before recommending this to anyone paying for it: the ratio of attempted to proved entry points, a cost per verified dependency, and the list of libraries where the proof failed. The published specifications for failed proofs are a partial substitute, and a better one than a marketing page, because they show the edge of the method.
The number I would watch is not 180 million but the 17%: reuse is what makes the cost fall toward something a normal project can pay, the way Mathlib grew to nearly 300,000 theorems. If that holds, the question in a year is which dependencies are worth proving once for everyone.
Sources
- Anthropic, LLMs are making formal software verification feasible at a much larger scale, Frontier Red Team, published October 22, 2026.
- Neural Minute, OpenAI publishes 372 math results, 42% machine-checked, published October 10, 2026, for the comparison.
- Named in the post and not linked here: Theorem, which built the semantics and the pipeline; Google’s OSS-Fuzz, which supplied the fuzz tests; Rocq, the proof checker; Verus.