LLMs enable large-scale formal verification of open-source libraries

A collaboration between Anthropic and Theorem showed that an AI model can now generate formal proofs for hundreds of real-world libraries without the years-long hand-crafting that has traditionally limited verification to a handful of mission-critical projects.

Using Claude, the team proved security properties at the RISC-V assembly level for 123 open-source projects, and the process uncovered bugs that had survived years of testing and even “trillions of test runs,” according to the authors. The following sections break down how the AI reduced the effort required, what exactly was proved, and why the results matter for anyone who ships low-level code.

LLMs shrink the human labor needed for formal verification

Formal verification has long been a specialist activity. The seL4 operating-system kernel, for example, required two person-years to implement but 20 person-years to verify, a ratio that has kept verification out of most development pipelines. The Anthropic research paper states that “LLMs can now produce formal proofs for real-world software fully autonomously” Anthropic research. By feeding source code directly to Claude, the system generated assembly-level proofs without the manual translation step that usually dominates the workflow.

The AI still works under a concrete set of assumptions: the program must be a single-threaded static binary, run on a RISC-V 1 CPU, have a fixed memory budget, and execute under a modeled Linux operating-system response.

Within those bounds, Claude writes the mathematical model, attempts the proof, and either succeeds or returns a counterexample that pinpoints a potential bug. The result is a repeatable pipeline that can be applied to new codebases as often as needed, turning a multi-year bottleneck into a task that finishes in hours.

What Claude actually proved

Claude’s most concrete achievement was proving that each compiled binary will always exit normally without triggering memory-safety errors or failing assertions for every input smaller than 64 MiB.

The proof holds for all 123 libraries, each built as a single-threaded static binary with a fixed memory budget on a RISC-V 1 CPU running Linux. In practical terms, the model guarantees that, under the modeled conditions, none of the examined binaries can crash due to out-of-bounds accesses, null-pointer dereferences, or violated assertions.

The verification artifacts for each library are publicly available, together with the RISC-V and OS semantics used in the analysis. Theorem also released a Claude skill that lets developers run the same pipeline on their own projects, effectively turning formal verification into a service rather than a one-off research experiment.

Bugs that survived massive testing

Even software that has been exercised billions of times can hide subtle defects. The authors cite the Linux kernel, which despite deployment on billions of devices, recently disclosed over 1,000 vulnerabilities.

In the 123-library study, Claude identified bugs that had escaped detection despite “trillions of test runs.” When a proof fails, Claude supplies a concrete counterexample that shows the exact input and state causing the violation. Developers can patch the offending code and rerun the verification until the proof succeeds.

These findings reinforce a well-known limitation of testing: exhaustive test suites can still miss low-level undefined-behavior bugs. Formal verification adds a mathematical guarantee that complements traditional testing, especially for code that interacts directly with hardware or relies on precise memory layout.

How the workflow fits into a typical development cycle

1. Compile to RISC-V assembly, The code is built as a static binary with a fixed memory budget.
2. Run Claude’s verification skill, Claude translates the binary into a formal model, applies the chosen security rules, and attempts a proof.
3. Inspect results, A successful proof yields a certificate that the binary cannot crash under the modeled conditions. A failed proof returns a counterexample that developers can use to locate and fix the bug.
4. Iterate, After fixing the bug, the pipeline is rerun, producing a new proof or a new counterexample.

Because each step can be scripted, the entire process can be integrated into continuous-integration pipelines. Teams can therefore catch memory-safety regressions early, before they reach production, without needing a dedicated formal-methods expert on staff.

Limitations and future directions

The current approach is bounded by several assumptions. It only handles single-threaded static binaries, a fixed memory budget, and a specific RISC-V 1 CPU model running Linux. Multi-threaded programs, dynamic linking, or different architectures are outside the scope of the published proofs.

The authors acknowledge that the technique is “still far away from fixing all possible bugs,” but they argue that the roadmap is clear: as model capabilities improve, the assumptions can be relaxed and the range of provable properties can expand.

Another practical limitation is the need for accurate OS and hardware semantics. The team published the RISC-V and Linux semantics they used, and Theorem offers to run the pipeline for other projects, but developers must trust that those semantics faithfully represent their target environment. Future work may involve tighter integration with hardware vendors and OS developers to ensure the models stay in sync with real-world implementations.

The takeaway

LLMs such as Claude can turn formal verification from a multi-year specialist effort into an automated pipeline that scales across hundreds of libraries. The model proved that each compiled binary will never crash for inputs under 64 MiB on a RISC-V 1 Linux system, and it exposed bugs that survived massive testing efforts. By embedding AI-driven verification into the development workflow, teams gain a practical path to stronger security guarantees early in the software lifecycle.