AI Proves Software Safety With 180 Million Lines of Code

Anthropic claims its Claude model can now mathematically prove that existing software code operates without error, a process that has historically required massive human effort. The company presented the work as a method to make AI-generated software more trustworthy, though it outlined strict limitations on what the proofs actually guarantee. The core conflict lies in replacing the slow, expensive labor of human experts with a rapid, automated system that still requires specific conditions to hold true.

Formal verification has long been too costly for widespread use. Experts once required 20 person-years to verify seL4, a small operating system kernel. Because of that expense, the technique was largely reserved for high-stakes environments like Airbus avionics software. This new approach attempts to break that cost barrier by using AI to handle the heavy lifting.

Anthropic’s Frontier Red Team partnered with Theorem to assign the proof work to Claude. Within weeks, the model generated approximately 180 million lines of mathematical proof code. It used test programs from 123 open-source libraries in Google’s OSS-Fuzz security project. The model did not write new software. Instead, it turned crash tests into mathematical problems, analyzed compiled machine code, and constructed the proofs.

A separate program called Rocq automatically checks these proofs. Anthropic states the process requires almost no human reviewers. The researchers described the generation as fully autonomous, noting that humans at Theorem built the underlying tools and formal foundations. During the work, Claude found hundreds of bugs and was allowed to fix them. Many of these errors likely would have escaped conventional testing because they only appear under narrow conditions, such as unusually large input files or specific access sequences.

In one test, the team found as many security bugs in a widely used PDF reader in one week as are usually reported for that software in a full year. In another application, Claude identified a logical error that had gone unnoticed for over a decade. The researchers note that even when a complete proof fails, the attempt can still reveal real bugs.

The proofs only hold under specific conditions: a particular processor architecture, single-threaded programs, and inputs smaller than 64 MB. Real-world deployments often run on different hardware. Cost remains a constraint, with individual proofs consuming hundreds of millions of tokens. Anthropic has not published total project costs, but it argues that if AI can verify its own code, developers can trust it more and spend less time reviewing.

A smaller test run showed that proofs can be reused. Efficiency is improving, with Opus 5.5 solving half the proofs using about 40 percent fewer tokens than Opus 5. Theorem’s roadmap now targets critical infrastructure, including glibc, OpenSSL, and cURL.