Anthropic and Theorem use Claude to generate formal proofs of correctness for 123 open-source libraries, finding hundreds of bugs

Anthropic's Frontier Red Team, working with a company called Theorem, says Claude wrote about 180 million lines of proof code in a few weeks. The proofs cover compiled machine code for test programs from 123 open-source libraries in Google's OSS-Fuzz, and the Rocq proof checker validated them. Anthropic says the work turned up hundreds of bugs, including a logic error undetected for over a decade, and as many security bugs in a widely used PDF reader in one week as are usually reported in a year. The proofs only hold for one processor architecture, single-threaded programs and inputs under 64 MB. This account comes via The Decoder's coverage of Anthropic's own post, and no primary links were captured.

If it holds up, this shows AI can produce machine-checked evidence that code behaves correctly, which is a stronger guarantee than testing. The proof checker is the credible part: a checked proof does not rely on trusting the model. Maintainers of open-source libraries and security teams are the most likely to benefit, mainly through the bugs found. The cost is high, though. Individual proofs use hundreds of millions of tokens, and the stated limits cover only a narrow slice of real software, so this is not yet something most teams can adopt.

The headline claim that Claude "writes code and proves it safe automatically" overstates it. What was shown is proofs of specific properties for test programs, under tight limits, not proof that arbitrary code is safe. The expectation that formal verification will become "as routine as testing" is a forecast from Anthropic, not a result. The bug counts and token savings (Opus 5.5 using about 40% fewer tokens than Opus 5) are the company's own figures with no independent check, and "hundreds of bugs" does not say how many were serious or confirmed by maintainers.

1. 01Whether Anthropic or Theorem publishes the proofs, the method and a bug list that maintainers of the affected libraries can confirm, including CVE numbers for the PDF reader bugs.
2. 02Whether Theorem delivers on its roadmap for glibc, OpenSSL and cURL, and whether the limits (one architecture, single-threaded, under 64 MB inputs) are loosened.
3. 03Actual cost per verified library in dollars and tokens, and whether outside researchers reproduce the results or compare them with existing tools such as seL4-style verification and fuzzing.