180 Million Lines of Proof: Claude Verifies Legacy Code

Formal verification has long been the gold standard for ensuring software reliability, yet the process has remained out of reach for most developers due to its extreme labor requirements. That dynamic is shifting rapidly as Anthropic announces that its Claude model has successfully generated mathematical proofs for existing code, marking a significant leap in the field of software assurance.

The scale of the output is staggering. In a matter of weeks, Claude produced approximately 180 million lines of mathematical proof code. This effort drew upon test programs from 123 open-source libraries within Google's OSS-Fuzz security project. By contrast, verifying seL4, a small operating system kernel, previously required specialists to invest 20 person-years of work. This historical burden is why formal verification was largely restricted to high-stakes environments like Airbus avionics.

The project involved a collaboration between Anthropic's Frontier Red Team and a partner called Theorem. The goal was to hand the complex proof work to the AI model. Claude did not write new software. Instead, it verified existing code by converting crash tests into mathematical problems. The model analyzed compiled machine code and constructed extensive proofs to demonstrate correct behavior under specific conditions.

A separate verification program known as Rocq automatically checks these proofs. Anthropic states that the process requires almost no human reviewers. The researchers describe the proof generation as fully autonomous, although they note that the underlying tools and formal foundations were built by humans at Theorem. This division of labor allows the AI to handle the heavy lifting while established systems ensure the mathematical rigor.

The work yielded immediate practical results beyond just theoretical assurance. During the process, Claude encountered hundreds of bugs and was permitted to fix them. The researchers indicate that many of these issues would likely have escaped conventional testing because they only appear under narrow conditions. These conditions include unusually large input files or specific sequences of memory accesses that are rare in standard use cases.

One particularly notable outcome involved a widely used PDF reader. The team found as many security bugs in a single week as are usually reported for that software in an entire year. In another application, Claude identified a logical error that had gone unnoticed for more than a decade. Anthropic adds that even when a complete proof fails, the attempt can still reveal real bugs, making the process valuable even without a full success.

Despite these successes, the company is careful to define the boundaries of the achievement. Formally verified does not mean error-free in all contexts. The proofs hold only under defined conditions, including a particular processor architecture, single-threaded programs, and inputs smaller than 64 MB. Real-world deployments of these libraries often run on different hardware and configurations, which may fall outside the scope of these specific proofs.

Cost remains a significant factor in the adoption of this technology. Individual proofs consume hundreds of millions of tokens, and Anthropic has not published the total project costs. However, the company argues that if AI can verify its own code, developers could trust AI-generated software more. This would allow teams to spend less time on manual review, potentially cutting costs across the broader coding process.

Efficiency is already improving, according to a smaller test run. Proofs can be reused, and the latest model, Opus 5.5, solves half the proofs using about 40 percent fewer tokens than Opus 5. This trend suggests that the financial barrier to entry may decrease over time as the models become more efficient at handling these complex mathematical tasks.

The project shifts the central question from whether AI can program to whether it can prove the code it writes is safe. Anthropic expects formal verification with AI to become as practical as standard testing in the near future. Theorem's roadmap already targets critical infrastructure components, including glibc, OpenSSL, and cURL, signaling a push to apply this technology to the foundational layers of modern software systems.