Claude wrote 180 million lines of proof. Read what it does not prove

Facts are attributed and linked to their sources. The analysis and opinions are the author's own.

What it is

On 22 October Anthropic's Frontier Red Team, working with a company called Theorem, published results from using Claude to write formal proofs about real software. Claude took fuzz tests from Google's OSS-Fuzz programme and proved that 239 entry points across 123 open-source libraries will not crash for any input smaller than 64 MB. The proofs work on the compiled RISC-V machine code, not the source code.

The scale is new. The proofs come to about 180 million lines of Rocq, a proof language, with a typical proof of about 600,000 lines covering a binary with a median of 18,000 instructions. For comparison, Anthropic notes that the seL4 kernel took two person-years to build and 20 person-years to verify. Along the way Claude found hundreds of bugs, including a rediscovery of CVE-2026-56132 in libexpat. In a separate experiment, a Python interpreter Claude wrote in Rust behaved identically to CPython on 99.95% of 1.7 million random programs.

Costs are falling. On 36 small verification tasks, Anthropic says Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5, and agents sharing a workspace of finished proofs needed 17% fewer tokens than agents working alone.

Why it matters

Most software assurance today is statistical: run enough tests and hope the gaps are small. A proof changes the question. Instead of trusting millions of lines of code, you trust a much smaller base: the formal models of RISC-V and Linux, the exact theorem statements and the Rocq proof checker.

A test tells you the inputs you tried were fine. A proof tells you every input is, as long as the model of the machine is right.

Anthropic is candid about the limits, and they matter. "'Formally verified' does not mean 'bug-free.'" The proofs assume single-threaded, static RISC-V binaries linked against musl libc, while most real deployments use x86 or ARM with glibc. AddressSanitizer does not catch every memory bug, and not every entry point was verified. My view is that the right reading is not "solved" but "affordable": proofs that used to be reserved for avionics now look like something a large buyer could ask for on its most critical open-source dependencies.

What I'd watch

• Whether formal models for x86 and ARM arrive, so the proofs cover the machines people actually run.
• Progress on Theorem's stated plan to verify the Nix ecosystem, including glibc, OpenSSL and cURL.
• Whether software buyers start asking vendors for proofs on critical components, not just test reports.