Anthropic's AI Just Proved Code Safe at a Scale Humans Couldn't Match

Anthropic has effectively changed the rules for software safety by using its Claude model to automatically mathematically verify code. Working alongside partner Theorem, the company demonstrated that AI can not only write software but also prove its correctness without human intervention. This development marks a significant shift from traditional testing methods, which often miss subtle errors, to a system that can guarantee safety under specific conditions. The approach allows for a level of automated assurance that was previously reserved for high-stakes, expensive projects like aviation systems.

To understand the scale of this leap, consider the history of formal verification. In the past, proving software was error-free was prohibitively slow. For instance, a team of specialists took twenty person-years to verify the seL4 operating system kernel. Because of this high cost, the method was rarely used outside of critical infrastructure like Airbus avionics. However, the recent collaboration between Anthropic’s Frontier Red Team and Theorem changed the timeline. In just a few weeks, Claude generated approximately 180 million lines of proof code. It drew from test programs in 123 open-source libraries within Google's OSS-Fuzz project, completing in days what would have taken human experts decades.

The process involved Claude translating crash tests into mathematical problems and analyzing compiled machine code to produce extensive proofs. An independent program called Rocq automatically checks these proofs, a workflow Anthropic describes as nearly free of human review. While the underlying tools and formal foundations were built by humans at Theorem, the actual proof generation is considered fully autonomous. During this work, Claude identified hundreds of bugs that conventional testing had missed. Many of these errors only appeared under specific conditions, such as unusually large files or specific access sequences. In one instance, the team found as many security bugs in a single week in a popular PDF reader as are typically reported in an entire year.

Despite the impressive results, there are practical limits to what this technology can do. Anthropic notes that 'formally verified' does not mean the software is entirely error-free. The proofs only hold under strict conditions, including specific processor architectures, single-threaded programs, and inputs smaller than 64 MB. Since real-world libraries often run on diverse hardware and configurations, these constraints matter. Additionally, the compute cost is significant, with individual proofs requiring hundreds of millions of tokens. However, newer models are becoming more efficient; Opus 5.5 solves half the proofs with about 40 percent fewer tokens than its predecessor, Opus 5.

The long-term impact is a shift in how developers trust AI-generated code. If AI can verify its own work, the cost of the entire coding process may drop significantly. Theorem’s roadmap already targets critical infrastructure components like glibc, OpenSSL, and cURL. Anthropic expects this type of formal verification to become as routine as standard testing. For now, the question for the industry is no longer whether AI can program, but whether it can prove that its code is safe, a hurdle it has now largely cleared.

This advance suggests that software automation is moving toward a new standard where correctness is guaranteed by mathematics rather than just tested by execution. While the current limitations require specific environments, the efficiency gains are clear. As models become more token-efficient and the scope of verification expands, the gap between writing code and proving it safe continues to close.