AI model generates 180 million lines of math to verify old code

Anthropic used its Claude model to mathematically prove that existing software code works correctly. The model generated approximately 180 million lines of mathematical proof code. This task previously required years of specialized human labor.

Formal verification is the practice of proving software runs without error in all scenarios. It has been too expensive for most developers. Specialists took 20 person-years to verify seL4, a small operating system kernel. As a result, the technique was mostly limited to high-stakes software like Airbus avionics.

Anthropic's Frontier Red Team partnered with a company called Theorem. They handed the proof work to Claude. In a matter of weeks, the model processed test programs from 123 open-source libraries in Google's OSS-Fuzz project. Claude did not write new software. It verified existing code by turning crash tests into mathematical problems. It analyzed compiled machine code and constructed the proofs.

A separate program called Rocq checks these proofs automatically. Anthropic states the process needs almost no human reviewers. The researchers describe the proof generation as fully autonomous. However, they note that humans at Theorem built the tools and formal foundations.

Claude found hundreds of bugs during the process and was allowed to fix them. Many of these errors would likely have escaped conventional testing. They appear only under narrow conditions, such as unusually large input files. While verifying a widely used PDF reader, the team found as many security bugs in one week as are usually reported in a full year. In another case, Claude identified a logical error that had gone unnoticed for more than a decade.

The company warns that formally verified does not mean error-free. The proofs hold only under defined conditions. These include a particular processor architecture, single-threaded programs, and inputs smaller than 64 megabytes. Real-world deployments often run on different hardware.

Individual proofs consume hundreds of millions of tokens. Anthropic has not published the total project costs. A smaller test run showed that proofs can be reused. Efficiency is improving. Opus 5.5 solves half the proofs using about 40 percent fewer tokens than Opus 5. Theorem plans to apply this method to critical infrastructure like glibc, OpenSSL, and cURL.