Anthropic uses Claude to prove existing code correct

Finding bugs while building proofs

Claude did not write new software. It translated crash-testing programs into mathematical problems, analyzed compiled machine code and generated detailed proofs. Rocq, an independent program, checked the results. Anthropic says reviewers were barely needed, though Theorem’s specialists built the tools and formal foundations the system relied on.

The process also surfaced hundreds of bugs, some of which Claude could fix itself. Researchers say many would have escaped ordinary testing because they appeared only in unusual conditions, such as unusually large files or particular sequences of data access.

Anthropic says an attempted proof can reveal a real bug even when verification does not finish.

The limits behind the guarantee

Anthropic cautions that “formally verified” does not mean “bug-free.” The proofs hold only for a specific processor architecture, single-threaded programs and inputs smaller than 64 MB. In practice, these libraries run on different hardware and in different configurations.

The cost is another constraint: individual proofs can consume hundreds of millions of tokens, and Anthropic has not disclosed the project’s total cost. I think that missing number matters as much as the bug count. A proof that finds more defects than a year of reported security issues is compelling; whether teams can afford to run that process routinely is a different question.

A small additional test suggests proofs can be reused and newer models can produce them more efficiently. Opus 5.5 solved half the proof tasks using about 40 percent fewer tokens than Opus 5.

From code generation to code assurance

The larger shift is not simply that AI can write code. If it can also establish that code meets a precise specification, developers may spend less time checking AI-generated software—and formal verification could reach beyond the high-stakes cases where it has traditionally been used. Anthropic expects AI-assisted formal verification to become as practical as standard testing.

Theorem’s roadmap names critical infrastructure including glibc, OpenSSL and cURL. That ambition raises the bar: the next question is not only whether models can produce proofs, but how much of the software those proofs actually cover.