AI verifies code with 180 million lines

180 million lines of mathematical proof code were generated by Anthropic’s Claude model in a matter of weeks. This massive output represents a significant shift in how software reliability is assessed, moving away from traditional manual testing toward automated mathematical verification. The work was conducted by the company’s Frontier Red Team in partnership with Theorem, aiming to demonstrate that AI can ensure the correctness of existing software.

Historically, formal verification has been a costly and time-consuming process reserved for high-stakes environments like aviation. For instance, verifying the seL4 operating system kernel required 20 person-years of expert labor. By contrast, the recent effort utilized test programs from 123 open-source libraries within Google’s OSS-Fuzz project. Claude did not write new code but instead analyzed compiled machine code, converting crash tests into mathematical problems to construct rigorous proofs.

The process relies on a separate verification program called Rocq to automatically check the generated proofs. Researchers describe the generation phase as fully autonomous, though they acknowledge that the underlying formal foundations and tools were built by humans at Theorem. Anthropic states that this approach requires almost no human reviewers, marking a departure from the heavy expert involvement previously required for such tasks.

During the verification process, Claude identified hundreds of bugs, which it was permitted to fix. Many of these issues likely would have been missed by conventional testing because they only appear under specific conditions, such as unusually large input files or specific access sequences. In one notable case, the team found as many security bugs in a widely used PDF reader in a single week as are typically reported in a full year. Additionally, Claude uncovered a logical error that had remained undetected for more than a decade.

Despite these successes, the company emphasizes that formal verification does not guarantee software is entirely error-free. The proofs are valid only under defined constraints, including specific processor architectures, single-threaded execution, and inputs smaller than 64 MB. Real-world deployments often vary in hardware and configuration, meaning these guarantees may not apply universally. Cost remains a factor, with individual proofs consuming hundreds of millions of tokens, although Anthropic notes that efficiency is improving as newer models like Opus 5.5 use fewer tokens to solve similar problems.

The initiative suggests a future where developers can trust AI-generated software more readily, potentially reducing the time and cost associated with manual code review. Anthropic expects this method to become as practical as standard testing in the near future. Theorem’s roadmap already includes plans to apply this verification to critical infrastructure components such as glibc, OpenSSL, and cURL, signaling a broader push toward securing the digital foundations of the internet.