Anthropic Uses Claude to Verify Security in 123 Software Libraries

Anthropic and a software checking company called Theorem have used Claude to mathematically check important security rules in 123 real open-source software libraries. Open-source software is code that people can freely view and use. The project shows how artificial intelligence (AI) could help check more software for problems. The project was announced on October 22, 2026. The team studied programs at the RISC-V assembly level, which means looking at the low-level instructions that a computer runs. They found bugs that had not been discovered even after a great deal of testing. According to Anthropic, as far as the company knows, this is the first large project to use AI and mathematical proofs to check real software at the assembly-code level.

The researchers also shared some of their mathematical proofs, along with the rules describing how RISC-V and the operating system work. This allows other people to check the results for themselves and use the work in other projects. These proofs show that the programs meet certain safety rules. They do not prove that the software has no bugs at all. Under specific conditions, the checked programs are guaranteed to finish normally, without making unsafe memory accesses or failing required checks. This guarantee covers every input smaller than 64 MB, every Linux operating system response included in the model, and every memory arrangement covered by the model.

These guarantees only apply when a program runs as a single-threaded static binary, meaning it uses one thread and has its needed code built into the program. It must also have a fixed amount of memory and run on a RISC-V1 CPU using Linux. Anthropic made clear that this method still cannot prevent or find every possible software security problem.

Formal verification is a way of using mathematics to prove that software follows clearly written rules. Developers first write down exactly how a program is supposed to behave. They then try to prove that it follows those rules in every situation covered by the check. If the proof fails, it may show that the program can do something that breaks the rules. This can help developers find a bug. They can fix the problem and run the checks again until they can prove that the program follows the required rules.

Anthropic said that making these proofs has traditionally been difficult and expensive, which has stopped many developers from using formal verification. The mathematical proofs can be many times longer than the program code itself. Creating them has usually required people with special skills and a lot of engineering time. Anthropic pointed to the seL4 operating system kernel, the central part of an operating system, as an example of how much work this can take.

Writing the seL4 kernel took two person-years of work, but formally verifying it took 20 person-years. A person-year means the amount of work one person would do in a year. Because this process takes so much time and effort, formal verification has mostly been used for software where mistakes could be especially dangerous, such as Airbus aircraft electronics software.

Claude also helped solve another difficult problem: deciding what correct behavior means for software that already exists. Many programs do not have complete, clear descriptions of exactly what they should do. To deal with this, the researchers took existing collections of software tests that could already be compiled and turned them into formal rules. These rules required the tests to pass every time. The researchers then combined these rules with a general mathematical model of how programs compiled for RISC-V run on Linux.

Anthropic said this allowed Claude to work out how programs containing tens of thousands of low-level assembly instructions would behave with different inputs and interactions. The company also said Claude found bugs that had gone unnoticed for years, even after trillions of test runs. These results show that mathematical proofs can find problems that ordinary software testing might miss. However, each proof only guarantees the specific rules and running conditions that it checks.

Besides checking the 123 software libraries, Anthropic described early experiments using other formal verification methods to solve more software security and development problems. These experiments included checking the security of the zlib compression algorithm, which helps make data smaller; proving that a Python interpreter written in Rust behaves the same way as the version it is meant to match; and looking into bugs that have existed for a long time in important software.

Theorem is offering to use the same verification process on other open-source projects. It is also releasing a Claude skill, a set of instructions that helps Claude carry out a task, so developers can start checking their own code. Anthropic also believes that reusing existing mathematical proofs and changing them to work with other programs could make formal verification cheaper across different software projects.