Anthropic worked with its partner Theorem to use its AI model Claude to mathematically prove that existing software code works correctly. The effort covered 123 open-source libraries included in Google’s security project OSS-Fuzz. In a few weeks, the system generated about 180 million lines of proof code and reportedly uncovered hundreds of bugs that conventional testing had missed.
The gap between “passed the tests” and “proven correct”
When people think about checking software quality, many think of testing: supplying prepared inputs and checking whether the expected results are returned. But testing can verify only the cases that have been tried. It cannot tell you how the software will behave in situations that have not been tested.
That is where formal verification comes in. It treats a program’s behavior as a mathematical problem and proves that the program will always work correctly within a defined set of conditions. In principle, it is powerful, but the effort required has been on an entirely different scale. Verifying the small OS kernel seL4, for example, reportedly took a team of experts a total of 20 person-years. It is no surprise that formal verification has been used mainly in extreme cases, such as control software for passenger aircraft.
Anthropic’s Frontier Red Team partnered with Theorem to hand this proof work to Claude. The model was not asked to write new code. Instead, it worked on existing software, recasting tests that look for crashes as mathematical problems, analyzing the code down to the machine instructions produced after compilation, and assembling proofs at scale.
A separate program serves as the proof “grader”
It would not be very convincing for an AI to declare its own proof a “pass.” The grading system used here is noteworthy. The generated proofs are automatically checked by Rocq, an independent verification program. According to Anthropic, this process requires almost no human review.
The research team calls this “fully autonomous” proof generation. However, the tools used for the proofs and their formal foundations were created by people at Theorem. Rather than saying the AI generated everything from scratch, it is more accurate to say that, on a playing field prepared by humans, the AI rapidly produced a vast number of proofs.
Hundreds of bugs uncovered along the way
As it worked through the proofs, Claude encountered hundreds of bugs and was allowed to fix them itself. According to the researchers, many surfaced only under narrowly defined conditions, such as extremely large input files or memory accesses in a particular order. It is easy to see how they could slip through ordinary testing.
The researchers cited specific examples. In an examination of a widely used PDF reader, a week of work uncovered as many security bugs as the software typically receives reports about over an entire year. In another application, they reportedly found a logic error that had gone unnoticed for more than 10 years.
Another important point is what happens when a proof is not completed. Anthropic says that even when a proof attempt fails, actual bugs can surface along the way. Proof work is not just a process for issuing a “certificate of passing”; it can also act like a probe for digging up bugs. Rather than replacing conventional testing, it appears to complement it by covering what testing misses.
Don’t overstate what “formally verified” means
That said, it is dangerous to equate “formally verified” with “bug-free.” Anthropic itself acknowledges that a proof holds only within strict conditions. The assumptions include a specific processor configuration, a single-threaded program, and inputs smaller than 64 MB. Real-world libraries run on a variety of hardware and settings.
The cost is not trivial, either. Individual proofs can reportedly consume hundreds of millions of tokens. The total cost of the project has not been disclosed. On the other hand, smaller follow-up experiments showed that proofs can be reused, and newer models appear to be becoming more efficient. Opus 5.5 reportedly uses about 40% fewer tokens than Opus 5 to solve half of the proofs.
The question shifts from “Can AI write programs?”
If AI can write code and conditionally guarantee that it is correct, the question changes. Instead of asking, “Can AI program?” we can ask, “Can AI prove the safety of the code it writes?” For development teams concerned about the reliability of AI-generated code, that is a significant shift. If AI can verify its own code, it could reduce the burden of human review and potentially cut costs not just for verification but across the entire development process.
Anthropic expects AI-based formal verification to become as commonplace as conventional testing in the near future. Theorem’s roadmap includes critical infrastructure software such as glibc, OpenSSL, and cURL.
What matters here may be the ability to examine not the “contents” of a proof, but its “assumptions.” What environment and inputs does the proof assume? In an era when even the checking is entrusted to AI, human literacy in verifying those assumptions may be the last line of defense for safety.
Comments