Aiming to achieve 'bug-free software,' Anthropic has developed a method that 'uses AI to mathematically prove that software is bug-free.'
As AI becomes more powerful, it is finding many bugs, or mistakes, in different kinds of software. Some of these bugs have caused serious problems, including one that led to an emergency update to PHP. Now, AI company Anthropic says it is working on a way to use AI to mathematically prove that software has no bugs. This method is called formal verification.
LLMs are making formal software verification possible on a much larger scale | Anthropic
https://www.anthropic.com/research/formal-verification
Formal verification is a way to use mathematics to prove that software code has no bugs. This idea has been around for a long time. However, creating these mathematical proofs takes a lot of work. Because of this, formal verification has mainly been used for very important systems, such as software that controls equipment on airplanes.
Anthropic worked with a research organization called Theorem to create a way to use its AI model, Claude, for formal verification. They tested this method on 123 open-source software libraries, which are collections of code that anyone can use and study. Claude kept finding and fixing bugs as it worked through the mathematical proofs. In the end, the researchers were able to mathematically prove that the software would not crash because of bugs under certain conditions. These conditions were that the program ran as a single-threaded static binary, meaning it used one thread of execution and was built as a self-contained program, with a fixed amount of available memory, on a computer running Linux with a RISC-V processor.
Formal verification can use more than 100 million tokens. Tokens are small pieces of text that AI models process, and using so many of them can be expensive. However, Anthropic believes these costs will gradually become lower for two reasons. First, as AI models get better, they should need fewer tokens to complete the same work. Second, different programs may need similar mathematical proofs. By reusing parts of proofs that have already been created, the AI may be able to finish new proofs using fewer tokens. The graph below shows how many tokens were used in 36 formal verification tasks. It shows that Claude Opus 5.5 completed the work using fewer tokens than Claude Opus 5.
Anthropic says formal verification still has some important limits. For example, proving that software has no bugs when running on a RISC-V processor does not mean it will be free of bugs on other types of processors, such as Arm or x86. To prove that software has no bugs in the real world, researchers would need to create mathematical models of every type of computer setup on which the software might run. Even with these challenges, Anthropic believes the limits can eventually be overcome as researchers learn more about using large language models, or LLMs, for formal verification and as the AI models continue to improve.
Theorem offers its LLM-based formal verification method to open-source projects for free. More information is available at the following link.
OSS Verify | Theorem
https://theorem.dev/oss-verify/
Theorem has also made the skills used for formal verification available to the public for free.
oss-verify/.claude/skills/add-project/SKILL.md at main · theorem-labs/oss-verify · GitHub
https://github.com/theorem-labs/oss-verify/blob/main/.claude/skills/add-project/SKILL.md