Anthropic Deploys AI to Automatically Prove Software Safety

For decades, proving that software is mathematically correct has been a luxury reserved for critical systems like aircraft avionics. The process is so expensive and labor-intensive that it rarely touches everyday code. However, a new collaboration between Anthropic and Theorem suggests that artificial intelligence could fundamentally change this dynamic by automating the verification process, potentially making rigorous safety checks a standard part of software development rather than an exceptional expense.

The core challenge lies in the sheer scale of effort required for formal verification. Historically, teams of specialists had to spend years on a single project. For instance, verifying the small operating system kernel seL4 took 20 person-years. This bottleneck meant that only the most safety-critical applications, such as those in aerospace, could afford the method. By applying large language models to this task, researchers are attempting to break the link between computational cost and verification reliability, allowing for broader application across the software ecosystem.

Anthropic’s Frontier Red Team worked with Theorem to have Claude perform this verification work autonomously. Rather than writing new applications, the model focused on analyzing existing code from 123 open-source libraries included in Google’s OSS-Fuzz security project. In a matter of weeks, Claude generated approximately 180 million lines of mathematical proof code. This massive output was used to translate crash tests into mathematical problems and analyze compiled machine code, creating a comprehensive record of correctness for the targeted software.

The process is designed to be largely hands-off. An independent verification program called Rocq automatically checks the proofs generated by Claude. According to Anthropic, this system requires very few human reviewers, leading researchers to describe the workflow as fully autonomous. While the underlying formal foundations and tools were created by humans at Theorem, the actual execution of the proof generation was handled by the AI. This shift implies a significant reduction in the human labor required to maintain high standards of software safety.

One of the most notable outcomes of this project was the discovery of numerous bugs that had evaded conventional testing for years. Claude identified hundreds of these errors and was permitted to fix them independently. Many of these flaws only manifested under specific, rare conditions, such as unusually large input files or particular sequences of data access. In one striking example, during the verification of a widely used PDF reader, the team found as many security bugs in a single week as are typically reported for that software in an entire year. In another case, the model detected a logical error that had remained undetected for over a decade.

Despite the impressive results, the method has clear practical limitations. Anthropic emphasizes that being formally verified does not mean the software is error-free in every possible scenario. The proofs are valid only under strict conditions, including specific processor architectures, single-threaded programs, and input files under 64 megabytes. Since these libraries often run on diverse hardware and configurations, the verification covers a specific slice of their operational environment rather than the entire range of possible use cases.

The computational cost of this approach remains high, with individual proofs consuming hundreds of millions of tokens. Anthropic has not disclosed the total project costs, but the efficiency gains are beginning to show. A smaller test run indicated that proofs are reusable, and newer models are becoming more efficient. Specifically, the Opus 5.5 model solved half of the required proofs using approximately 40 percent fewer tokens than its predecessor, Opus 5. This trend suggests that the cost barrier may lower over time, making the technology more accessible to a wider range of developers.

The broader implication is a shift in how the industry views AI-generated software. If AI can not only write code but also prove its correctness under defined conditions, developers can trust automated outputs more readily. This could reduce the time spent on manual review and lower the overall cost of the coding process. The question is moving from whether AI can program to whether it can guarantee safety, a step that could transform software automation beyond current coding tools.

Looking ahead, Anthropic expects formal verification with AI to become as routine as standard testing. Theorem’s roadmap already targets critical infrastructure components like glibc, OpenSSL, and cURL. If these efforts succeed, the software development lifecycle could undergo a major transformation, where mathematical proof of safety becomes a standard deliverable rather than an exceptional achievement.