Claude’s AI verifies 123 real-world libraries

Claude has generated formal security proofs for 123 open-source libraries, in an experiment by Anthropic and Theorem that brings formal verification from highly specialized projects to software used in the real world.

Formal verification attempts to prove that a program follows certain rules in every covered case, not just in the examples someone has tested. In theory, it can provide much stronger guarantees than running millions of tests. In practice, writing those proofs has required years of expert work.

Anthropic says Claude automated a substantial part of that process. The model worked on compiled programs, meaning the instructions executed by the processor, rather than only on the original source code.

What Claude managed to prove

The team turned existing security tests into a formal specification. The rule was specific: certain programs must not crash, fail an assertion, or cause memory safety errors for any input smaller than 64 MB.

Claude performed this work on 239 entry points across the 123 libraries. An entry point is the function or interface through which a test feeds data into a program. The analysis covered compiled binaries for the RISC-V architecture, using a formal model of the Linux operating system.

The guarantees come with important conditions. The programs were analyzed as static, single-threaded binaries, with a fixed amount of memory, running on a RISC-V processor. This does not mean the same proof automatically covers how those libraries work on x86 computers, ARM devices, or systems with libraries linked in a different way.

Even with those limitations, the volume is notable: the generated proofs add up to around 180 million lines of Rocq, the formal language and checker used to review the proofs. An independent checker validates that the proof matches the written specification exactly.

It also found old bugs

Claude did not simply try to prove that the code was safe. When a proof failed, the model investigated why, proposed a patch, and ran the process again with the corrected version.

That process uncovered hundreds of bugs, including some that traditional tools had little chance of finding. They included:

• A counter overflow in a decompressor that could cause an out-of-bounds write with inputs of around 20 MB and a very specific layout.
• An out-of-bounds read in an image decoder that required a 64 MB input and more than 2 GB of memory.
• An error that appeared only after a specific sequence of calls on two handles for the same file.
• A logic flaw that allowed files to be loaded even though a function was supposed to restrict which files were permitted.

The analysis also rediscovered vulnerability CVE-2026-56132 in libexpat, according to Anthropic. Some of these cases could evade fuzzers, tools that generate large numbers of modified inputs in an attempt to trigger failures. Testing many inputs helps, but it does not guarantee that every possible program path will be explored.

This does not mean the software is infallible

The distinction is essential: a formal proof does not show that a library is free of every possible bug. It shows that the library meets a specific specification within a specific machine model and under defined conditions.

If the specification leaves out something important, the proof will not cover it. It also will not detect a problem in the processor, the operating system, or the formal model itself. And proving that certain entry points do not fail is not the same as verifying every function, every possible use of the library, or the entire program that uses it.

In this experiment, the checks also focused on inputs smaller than 64 MB and on errors that the AddressSanitizer system could detect. Some memory vulnerabilities are invisible to that tool, and an application can use a library incorrectly even if the library has passed its tests.

What changes for software development

Until now, formal verification has been mostly reserved for systems where a failure could cost lives or enormous amounts of money. The team cites one well-known case: formally verifying the seL4 kernel required approximately 20 person-years, compared with the two person-years needed to implement it.

If AI models reduce that cost, companies could apply formal proofs to shared components such as encryption libraries, compressors, document readers, or networking tools. A single verified library could provide reusable guarantees to thousands of applications that depend on it.

There is still a practical obstacle: generating these proofs consumes hundreds of millions of tokens and substantial computing time. Anthropic says Opus 5.5 solved half of a set of 36 tasks using around 40% fewer tokens than Opus 5. When several agents shared partial proofs, they needed 17% fewer tokens than when working separately.

The next step will be bringing formal models closer to the systems you actually use, including x86 and ARM processors, dynamic libraries, and multithreaded programs. The promise is not that Claude will certify any application with one click, but that verification will stop being a task reserved for a handful of specialists and start becoming part of normal development, alongside testing and code analysis.