# Anthropic's Claude formally verifies existing open-source code with partner Theorem

published: 2026-10-23T12:05:41.429Z
topic: infrastructure
source: https://the-decoder.com/anthropics-claude-now-writes-code-and-proves-it-safe-automatically/
url: https://aiagentnews.io/stories/anthropic-s-claude-formally-verifies-existing-open-source-code-with-partner

Anthropic and Theorem used Claude to generate formal mathematical proofs of correctness for existing open-source libraries. The work produced roughly 180 million lines of proof code and surfaced hundreds of bugs that conventional testing had missed.

Formal verification has long been too expensive for most software, with one team reportedly needing 20 person-years to verify the seL4 kernel. Anthropic's Frontier Red Team, working with Theorem, had Claude do the proof work instead, using test programs from 123 open-source libraries in Google's OSS-Fuzz project. Claude turned crash tests into mathematical problems and analyzed compiled machine code, and an independent checker called Rocq verifies the resulting proofs automatically.

Claude also fixed the bugs it found along the way. In one effort to verify a widely used PDF reader, the team found as many security bugs in one week as are typically reported for that software in a full year. Anthropic says even proofs that fail still expose real bugs, and Claude caught a logic error that had gone unnoticed for more than a decade.

The proofs only hold under strict conditions: a specific processor architecture, single-threaded programs, and inputs under 64 MB. Compute costs are high, with individual proofs using hundreds of millions of tokens, and Anthropic did not report total project costs. A smaller test showed proofs can be reused, and Opus 5.5 solved half the proofs with about 40 percent fewer tokens than Opus 5.

## Why it matters if you build agents

Agents that generate code could in principle ship machine-checked proofs for narrow, defined conditions, which could cut review time. The guarantees only apply under the stated architecture, threading and input limits, so code that runs on other hardware or configurations is not covered. Budget for high token costs if you try this approach.