Anthropic Proved Memory Safety for 123 C Libraries at the Assembly Level, Using Claude

Anthropic’s Frontier Red Team, working with the verification startup Theorem, published research on October 22 claiming a first: large-scale formal verification of production software at the assembly level, with Claude writing the proofs and the Rocq proof assistant checking them mechanically. The scale: security properties proved for 239 fuzz-test entry points across 123 open-source OSS-Fuzz libraries, producing roughly 180 million lines of Rocq, about 600,000 lines per proof, covering binaries with a median of 18,000 RISC-V instructions. The property proved for each is the one C developers actually care about: the program always exits normally with no memory-safety errors or assertion failures, for any input under 64 MB.

How fuzz tests became formal proofs

The method is the clever part. Rather than writing new specifications, the team converted each project’s existing fuzz tests into formal statements, essentially “this test suite must always pass,” interpreted over Theorem’s RISC-V and Linux process semantics. Claude then wrote proofs against those statements, the Rocq checker verified them, and any real bugs the process surfaced were patched by Claude and re-proved, with penalties applied for reward hacking. The trusted computing base is small and explicit: the RISC-V/Linux semantics, the theorem statements, and the Rocq checker itself. This is the verification analogue of what we saw in Claude tracing the NIST curve seeds: the model does the exploratory, high-context work while a mechanical checker holds the ground truth.

What it found that trillions of fuzz tests did not

The bug list justifies the entire approach. Fuzzing had run trillions of test cases against these libraries, yet the proofs surfaced a counter underflow triggering out-of-bounds writes only on inputs near 20 MB, a bug requiring 64 MB inputs plus 2 GB of memory to manifest, and an independent rediscovery of CVE-2026-56132 in libexpat. They also found logic bugs that never crash at all, like a file-access restriction not always being enforced, which fuzzing cannot see by construction. Two further case studies extend the claim beyond C: the Linux kernel’s zlib was proven equivalent to the RFC 1950 specification at the x86 binary level (using Claude-generated x86 semantics), and a Rust Python interpreter proved in Verus matched CPython’s behavior on 99.95% of 1.7 million random test programs. In a separate PDF-reader effort, the team found a year’s worth of security bugs in one week, including a logic bug latent for a decade.

The economics, and the honest limits

Verification has always lost on cost, and the paper attacks that directly: Opus 5.5 proves half of a 36-task benchmark with about 40% fewer tokens than Opus 5, agents sharing a workspace used 17% fewer tokens, and proofs were heavily reused across similar programs, so the marginal cost of verifying library N+1 falls as N grows. The limitations section is refreshingly concrete: proofs cover single-threaded static RISC-V binaries with musl libc, not the x86/ARM-plus-glibc deployments most of the internet actually runs; “formally verified” means the spec matches, not that the software is bug-free; caller misuse is out of scope; and the proofs cost hundreds of millions of tokens. The team’s roadmap, package-level verification across the Nix ecosystem including glibc, OpenSSL, and cURL, is where this stops being a stunt. Read it next to the Postgres 19 delay: AI review finds bugs faster than humans can triage, and machine-checked proofs are the only triage mechanism that scales at the same slope as generation. If verification becomes as routine as fuzzing, as the authors expect, the economics of shipping C changes permanently.