AI model automatically certifies software safety in weeks

The software industry has long grappled with the high cost of ensuring code works flawlessly under every possible condition. Today, a significant shift occurred as Anthropic and its partner Theorem revealed that their AI model, Claude, can now mathematically verify existing software and generate formal proofs of its correctness.

This development marks a departure from traditional AI coding tools, which typically focus on writing new code. Instead, this system validates current software by translating crash tests into mathematical problems. The approach addresses a core challenge in AI-generated software: proving that the output is reliable without requiring extensive human review.

The scale of the operation was substantial. In a matter of weeks, the model produced approximately 180 million lines of proof code. This work covered 123 open-source libraries drawn from Google's OSS-Fuzz security project. For context, previous efforts to formally verify a small operating system kernel called seL4 required 20 person-years of specialist labor, a duration that made such rigorous checks viable only for critical systems like aviation software.

The process involved analyzing compiled machine code and generating extensive mathematical proofs. These proofs were then checked by an independent verification program named Rocq. According to Anthropic, the workflow requires almost no human reviewers, leading researchers to describe the proof generation as fully autonomous. However, the underlying formal foundations and tools were still designed by human experts at Theorem.

Beyond verification, the system identified and corrected numerous defects. Claude encountered hundreds of bugs during the proof generation process. Many of these issues had evaded conventional testing because they only manifested under specific conditions, such as unusually large input files or particular sequences of memory access.

One notable instance involved a widely used PDF reader. In a single week, the team found as many security bugs as are typically reported for that software in an entire year. In another case, the model uncovered a logical error that had remained undetected for more than a decade. Anthropic notes that even when a complete proof fails, the attempt often surfaces real bugs.

Despite these successes, the company emphasizes that formal verification does not guarantee software is entirely error-free. The proofs are valid only under strict conditions, including a specific processor architecture, single-threaded execution, and input files smaller than 64 megabytes. Real-world applications often run on varied hardware and configurations, meaning these proofs have practical limits.

The computational cost of this verification is also significant, with individual proofs consuming hundreds of millions of tokens. While Anthropic has not disclosed the total project cost, the efficiency gains are evident. A smaller test run showed that proofs are reusable and that newer models are more efficient; Opus 5.5 solved half the proofs with about 40 percent fewer tokens than its predecessor, Opus 5.

If AI can verify its own code, developers can place greater trust in automated software generation. This shift could reduce the time and cost associated with manual code review. The project suggests that the industry question may move from whether AI can program to whether it can prove its code is safe.

Anthropic expects this method to become as routine as standard testing. Theorem’s roadmap already targets critical infrastructure components, including glibc, OpenSSL, and cURL, indicating a move toward verifying the foundational software that powers the internet.