What was actually proved
Anthropic’s Frontier Red Team, working with Theorem, published results on 22 October from an attempt to use Claude for formal verification at scale. The team took existing fuzz tests from Google’s OSS-Fuzz, treated each test as a property the code must satisfy, compiled it to RISC-V assembly, and had Claude write machine-checked proofs that the resulting binary never crashes.
The property is narrow and precise: for any input under 64 MB, the program will not crash with a memory-safety error or a failed assertion. The proofs assume a single-threaded static binary with a fixed memory budget running on a RISC-V CPU under Linux, and they trust the Rocq proof checker, Theorem’s RISC-V and Linux process semantics, and the hardware and OCaml compiler beneath them.
The numbers
Across 123 open-source libraries, Claude proved 239 entry points free of crashes under that specification. The proofs total roughly 180 million lines of Rocq. A typical one runs to about 600,000 lines, against a median binary length of about 18,000 RISC-V instructions. The work took a few weeks.
Anthropic does not say how many entry points were attempted in total, so the figures do not support a success rate. The company says it is publishing proofs for the fuzz tests that needed no patching, and specifications for the ones it could not prove.
Hundreds of bugs turned up along the way, and Claude patched them, which regenerated the specifications. The examples given include a counter underflow in a decompressor that causes an out-of-bounds write only on a rare layout of about 20 MB of input, an out-of-bounds read in an image decoder that needs a 64 MB input and more than 2 GB of memory, and a rediscovery of CVE-2026-56132 in libexpat. One was a file-restriction feature that was not always enforced: a logic bug that never crashes, latent for more than a decade.
The obvious cheat, and what they did about it
The setup contains a hole the team names itself. Claude could make a theorem provable by rewriting the program so that it never crashes. Anthropic says it penalised patches that changed behaviour, gave extra credit for proving which inputs a patch changes, and logged and audited every patch.
Cost is the open problem
On a benchmark of 36 small verification tasks built from real OSS-Fuzz code, with three independent attempts at a five-million-token budget each, Opus 5.5 proved half of them using about 40% fewer tokens than Opus 5. Agents allowed to copy each other’s proofs from a shared workspace used 17% fewer tokens and completed 34 of the 36, against 32 for agents working alone.
Anthropic is explicit about the limits. “Formally verified” does not mean bug-free: a proof checker cannot confirm that the specification matches reality, and bugs can remain in the spec, the machine model or the trusted base. The proofs cover RISC-V binaries linked against musl, while most deployments run x86 or ARM with dynamically linked glibc. And a single proof can cost hundreds of millions of tokens, which the company calls a key open problem.
Separately, Claude wrote a specification from RFC 1950 and proved that the Linux kernel’s zlib implementation meets it at the x86 binary level. Anthropic says it repeated that for about six other widely used libraries. Whether that x86 work generalises further is the thing to watch.
