On October 22, 2026, Anthropic and Theorem announced that they had used the AI model Claude to mathematically prove, under specified conditions, that 239 test entry points across 123 open-source libraries do not crash. A test entry point is a test program that accepts various inputs and calls a library's functions. Conventional fuzzing hunts for bugs by feeding a program large numbers of actual inputs. This research instead proves that no error occurs for every input meeting the stated conditions, including inputs that were never actually tried. However, the proofs assume a specific executable and execution environment, and the published proofs do not guarantee that a program always terminates.
The work stands out because AI applied formal verification, which has traditionally demanded enormous effort from experts, to existing software at scale. At the same time, the conditions under which the proofs hold are strictly defined. They do not guarantee the safety of entire libraries, nor behavior in ordinary PC or server environments. Understanding exactly how much was proved, and under what conditions the guarantees hold, is essential to evaluating this research.
Turning Existing Fuzzing Tests into Proofs Over All Inputs
Instead of having humans write formal specifications of software from scratch, the researchers reused existing tests that developers had prepared for Google's OSS-Fuzz. Fuzzing is a testing technique that feeds a program randomly generated inputs, or mutations of existing ones, to look for problems such as crashes. Running it more often can uncover many bugs, but it cannot try every possible input. Formal verification, by contrast, describes mathematically the properties a program should satisfy and proves that those properties hold for all inputs within the target scope. This research converts the condition that an existing fuzzing test does not fail into a formal specification, and tries to show that the same property holds even for inputs that were never actually run.
According to Anthropic's research announcement, the team completed proofs for 239 test entry points in 123 open-source libraries within a few weeks, after fixing bugs along the way. The resulting Rocq proofs total roughly 180 million lines, and the target was executables compiled for RISC-V. Claude writes the proofs, and the Rocq kernel mechanically checks whether each proof actually derives the stated property. In other words, the AI's own judgment that something is "correct" is not simply accepted; an independent proof checker confirms it. The achievement is applying formal verification, long hindered by the heavy workload it places on experts, to existing software at scale.
When existing tests serve as the specification, what can be proved depends on what those tests check. For example, the compression library LZO has a test that confirms data compressed and then decompressed returns to the original. This test fails if the decompressed data does not match the input, so proving that the test never fails guarantees not only that no invalid memory access occurs, but also the functional property that compression and decompression results match. Still, what can be proved is only the conditions built into the test. The AI did not automatically discover requirements that the tests do not describe and guarantee the correctness of the software as a whole.
What the Published Proofs Guarantee, and Their Limits
The GitHub repository published by Theorem contains machine-checkable proofs for 60 test entry points in 25 libraries. This is a subset of the 123 libraries and 239 entry points claimed for the research as a whole. Anthropic limited the public release to proofs for tests that required no bug fixes, so not all of the research results are public. The scale of the announced results should therefore be distinguished from the scope that third parties can verify through the public repository.
An important point for understanding the proofs is the difference between an executable with AddressSanitizer (ASan) built in and a regular executable. ASan adds checking code to a program to detect problems such as invalid memory access. But proving that the instrumented program raises no errors does not by itself guarantee that the regular build behaves the same way. The team therefore made it part of the proof that both the instrumented and regular builds raise no errors and that their externally observable behavior matches. The public repository includes proofs targeting not only ASan but also UndefinedBehaviorSanitizer (UBSan), which detects undefined behavior.
On pages 1–2 of Anthropic's technical appendix (PDF), the property is defined for inputs under 64 MiB and an assumed memory layout: the regular and ASan builds raise no errors, and their observable behavior matches. The individual theorems in the public repository, however, carry separately stated assumptions, such as the regular build's execution fitting within a specified memory budget. The 64 MiB input limit in the technical appendix therefore cannot be applied uniformly to every published theorem. To judge the conditions under which a proof holds, you need to check the statement of each theorem.
"Observable behavior" here means things like data read and written through standard input and output, the program's exit status, and the final state of the file system. The proofs show that the instrumented and regular builds match on these externally checkable results. They do not guarantee identical processing speed or memory consumption. Moreover, proving behavioral equivalence does not guarantee that a program always terminates, because the properties to be proved differ between a program that falls into an infinite loop and one that finishes normally.
In the description of its public repository, Theorem states that this release contains no proof guaranteeing termination of execution and does not rule out the possibility of non-terminating runs. This does not mean an infinite loop was actually found; it means the proofs do not establish that every execution necessarily terminates. It is therefore inaccurate to read the result as "guaranteed to terminate normally on any input."
| Category | What the proofs cover and conditions to check |
|---|---|
| Scope of results | 123 libraries and 239 entry points across the research; 25 libraries and 60 entry points in the public release |
| Target environment | Single-threaded, statically linked, musl-based RISC-V executables for Linux |
| Theorem assumptions | Input limits, memory usage caps, and so on. How far OS system-call failures are tolerated also varies by theorem |
| Properties proved | Absence of errors under the stated conditions, and equivalence of observable behavior between the regular and instrumented builds |
| Not guaranteed | Termination of all executions in the public release; correctness of unverified entry points or code unreachable from the tests; safety including misuse by callers |
Because the proofs target specific RISC-V executables, they cannot be applied as-is to the same libraries compiled for x86 or ARM. The same guarantees do not necessarily hold for configurations that use glibc or programs that use dynamic linking. Nor can bugs of kinds that ASan and UBSan cannot detect be ruled out by proofs based on those checks. Proving the safety of some of a library's test entry points does not mean verifying code that is never executed from those entry points, or misuse on the part of applications that call the library.
Furthermore, even if a proof passes mechanical checking, that does not unconditionally guarantee the correctness of every element underlying the verification. These proofs depend on formal models that mathematically describe RISC-V instructions and the behavior of Linux processes. Beyond the requirement that these models accurately represent the behavior of real systems, one must trust the theorem statements, the Rocq kernel, and the tools that import executables into the model. Even as AI becomes able to generate vast quantities of proofs automatically, deciding what to verify and under what assumptions to prove correctness remains just as important.
A Memory-Corruption Bug Exposed by a Roughly 20 MB Special Input
Another important outcome is that hundreds of bugs were found while the proofs were being written. According to Anthropic, when Claude found a problem in an existing implementation while attempting a proof, it fixed the code and then wrote the proof again for the corrected program. Not only the finished proofs but the very process of trying to make them go through led to the discovery of defects that conventional tests had missed.
One particularly interesting case was a bug found in a decompressor. When a relatively large input of about 20 MB took a particular layout, a counter underflowed below its lower bound and led to a write outside the memory region. Typical fuzzing often repeatedly mutates relatively small inputs, and OSS-Fuzz may usually cap input size at around 1 MB. A bug like this one, which requires about 20 MB of data in a special arrangement, was therefore likely hard to find with conventional fuzzing.
To find a bug through fuzzing, you have to actually generate the problem-causing input and feed it to the program. Formal verification instead tries to show that a stated property holds for every input in scope, so conditions that ordinary tests rarely reach also come under examination. In this case, simply entering about 20 MB of data was not enough to trigger the bug; specific conditions, including the layout of the data, were required. Being able to find bugs with such complex conditions is one advantage of combining formal verification with existing tests.
Anthropic also reported rediscovering "CVE-2026-56132," a known vulnerability in libexpat triggered by deeply nested input. The hundreds of bugs found were not all previously unknown vulnerabilities; some were known issues. In another library, a logical bug that causes no crash was also found: a feature restricting which files may be read was not applied correctly under some conditions. This shows that working on proofs can reveal problems beyond memory safety, the property originally targeted.
Still, these results do not mean that formal verification can find every logic bug. The proofs deal only with predefined properties and the range of their assumptions. What this research showed is the possibility of discovering, in the course of writing mathematical proofs, defects that existing tests tend to miss, and of guaranteeing a certain level of safety for the corrected programs.
Can 180 Million Lines of Proof Extend to More Complex Software?
The roughly 180 million lines of proof produced in this research are notable in their own right. However, this figure does not count only proofs that Claude wrote line by line the way a human would. According to Anthropic's technical appendix, more than half of the successful proofs consist of data generated by tools Claude built itself, including instruction-encoding information and lookup tables. The remainder also includes script-generated content, and counting unsuccessful attempts, the Rocq code generated reached about 1 billion lines. The line count therefore cannot be compared directly with human effort or with the complexity of the programs being verified.
The lack of proportionality between proof length and target code size is also distinctive. According to the technical appendix, a proof of about 630,000 lines was produced for a 391-line parser test entry point in cJSON, while about 480,000 lines of proof were produced for fftw3, which contains roughly 51,000 lines of code. The proofs must also handle not just the target library's processing but program startup, the C standard library's memory management, the ASan runtime, and the fuzzing driver. That is why proofs can become enormous even when the library's own code is short.
Human formal-verification experts often abstract common processing and structure proofs so as to avoid repeating the same reasoning. The proofs Claude wrote, however, tended to describe in fine detail things like the contents of CPU registers, relationships between memory addresses, and behavior at each branch. According to the research team, checking a single proof alone takes from 30 minutes to several CPU-hours. Whether the current approach of generating large quantities of verbose proofs will work for larger and more complex programs is an important question going forward.
One solution is to reuse proofs about shared components. These proofs include parts common to many targets, such as program initialization and the ASan runtime. If the correctness of such processing is proved once and can be used for other programs, the same proof no longer has to be rebuilt for each target. This could widen the scope of verification while holding down the size of proofs and the computing resources needed to check them.
Theorem also points in this direction in "Bootstrapping the Verified Software Stack". The company envisions using the dependency relationships in the Nix package management system to proceed with formal verification starting from foundational shared libraries, then reusing those results in the software that depends on them. By accumulating proofs of common components, it aims eventually to extend verification to complex software as a whole. This is a future development plan, however, and verification of the Nix software collection as a whole has not been completed at this point.
An environment for third parties to verify the results has also been prepared. The public repository provides procedures for checking the proofs with the official Rocq 9.2.0, and lets users confirm the configuration of the target executables and the conditions under which the proofs hold. Still, these results rest on the research announcement and published materials from Anthropic and Theorem, not on independent third-party re-verification of all the proofs. When applying this in actual development, it is essential to check not just whether a library you use is among the verified targets, but also which version of the executable is covered, which test entry points the guaranteed behavior goes through, and what assumptions are required.
This achievement shows that AI-driven formal verification may apply not only to small research programs but also to open-source software in actual use. At the same time, its guarantees depend on specific executables, formal models, and theorem assumptions, and do not unconditionally ensure the safety of software as a whole. If proofs of common components can be reused in the future and verification extended to builds and execution environments in real use, a path may open for building formal verification into everyday software development.