Anthropic's Claude now writes code and proves it safe automatically

Anthropic used its AI model Claude to prove with math that existing software code works correctly. This could help solve a major problem with AI-written software, but the method still has important limits.

Proving that software will work without errors in every possible situation has always been extremely expensive and time-consuming. For example, a team of experts needed 20 person-years of work to mathematically check seL4, a small but important part of an operating system. That means an amount of work equal to one person working for 20 years. Because this process takes so much effort, it has mostly been used for software where mistakes could be especially dangerous, such as software used in Airbus aircraft electronics.

Anthropic's Frontier Red Team worked with a company called Theorem to let Claude do this difficult proof work instead. In just a few weeks, Claude produced about 180 million lines of mathematical proof code. It used test programs from 123 open-source software libraries included in Google's OSS-Fuzz security project.

Claude did not write new software in this project. Instead, it checked software that already existed. It took tests designed to make programs crash and turned them into math problems. It then studied the machine code that computers actually run and created detailed mathematical proofs. Another program, called Rocq, automatically checks whether those proofs are correct. According to Anthropic, the process needs almost no human reviewers. The researchers describe it as "fully autonomous," meaning it can create proofs on its own. However, people at Theorem built the tools and mathematical systems that make this possible.

Claude finds bugs that years of testing missed

While creating these proofs, Claude discovered hundreds of software bugs. It was also allowed to fix them on its own. The researchers say many of these problems would have been missed by normal testing because they only happen in unusual situations. For example, a bug might appear only when a program opens an extremely large file or when certain parts of the software are accessed in a particular order.

In one example, the team tried to prove that a widely used PDF reader worked correctly. In just one week, they found as many security bugs as people normally report for that software in a whole year. In another program, Claude discovered a mistake in the program's logic that nobody had noticed for more than ten years. Anthropic says that even when Claude cannot finish a complete mathematical proof, trying to create one can still reveal real software bugs.

What mathematical verification can and cannot do

Anthropic admits that calling software "formally verified" does not mean it has no errors. Formal verification means using math to prove that software behaves correctly under certain rules and conditions. In this project, the proofs only apply under strict limits: the software must run on a particular type of processor, it must use only one thread of execution at a time, and its inputs must be smaller than 64 MB. In the real world, these software libraries run on different types of hardware and with different settings. That means the proofs do not cover every way the software might be used.

The process also requires a lot of computing power. Some individual proofs use hundreds of millions of tokens, the small pieces of text and code that AI models process. Anthropic has not said how much the entire project cost. Still, if AI can check the correctness of code it writes, developers could have more confidence in AI-generated software and spend less time checking it themselves. This could reduce costs not only for checking software but also for the whole process of writing it. A smaller experiment also showed that mathematical proofs can be reused. Newer AI models are becoming more efficient, too. Anthropic's Opus 5.5 model can solve half of the proofs using about 40 percent fewer tokens than Opus 5.

This project provides more evidence that AI could automate much more of software development. If AI can both write code and prove that the code works correctly under clearly defined conditions, the main question changes. Instead of asking, "Can AI write software?" people may start asking, "Can AI prove that the software it writes is safe?" If AI can do that, the effects could be much bigger than what today's AI coding tools can achieve.

For example, Anthropic believes that using AI to mathematically verify software will soon become about as practical as ordinary software testing. Theorem's future plans already include checking important software components such as glibc, OpenSSL, and cURL. These are widely used tools that support many other programs and computer systems.