Anthropic has shown that its Claude models can perform formal software verification—a notoriously labor-intensive process of mathematically proving code is free of certain bugs—across more than 100 real-world open-source libraries. Working with the startup Theorem, the company proved security properties at the assembly code level for 123 projects, and in the process, Claude uncovered bugs that had survived years of conventional testing. The result suggests that a technique once reserved for mission-critical systems like avionics software could soon become a standard part of everyday software development.

Why formal verification has stayed niche until now

Most software is tested rather than proven. Developers write tests, run fuzzers, and rely on code review to catch bugs, but none of these approaches can guarantee that a program has no bugs left. Formal verification is different: it involves translating code into a mathematical model and proving that it always satisfies a defined set of rules. If the proof fails, the failure itself hints at where a bug might be. Fix it, try again, and repeat until the proof succeeds—at which point you have a mathematical guarantee that the code can’t violate those rules.

The catch is cost. Anthropic notes that building the seL4 operating system kernel took about two person-years, but formally verifying it took roughly 20 person-years of specialized expert labor. That ratio has kept formal verification confined to a handful of extremely high-stakes projects, such as Airbus’s avionics code, while the vast majority of software—including widely used, heavily tested systems like the Linux kernel, which recently had over 1,000 vulnerabilities disclosed—ships without any such guarantee.

What Anthropic and Theorem actually did

In this project, Anthropic asked Claude to autonomously produce correctness proofs for 123 open-source libraries. Specifically, Claude proved that certain executable artifacts from these libraries will always exit normally, without memory-safety errors or failed assertions, for every input under 64 MB. The proofs held across every modeled Linux OS response and memory layout, under a defined set of assumptions: the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU under Linux.

That’s a meaningful but bounded guarantee—it doesn’t mean these programs are bug-free in every possible scenario, only within the specific conditions the proofs cover. Still, Anthropic describes this as the first large-scale effort to apply AI-driven formal verification to production software at the assembly code level, rather than at a higher-level, more abstract representation of the code. Verifying at the assembly level is significant because it closes the gap between what gets proven and what actually runs on the hardware, removing potential discrepancies introduced by compilers.

How this differs from existing bug-finding approaches

Tools like fuzzers, static analyzers, and even AI-powered code review assistants can find bugs, but they can’t prove the absence of bugs—they can only fail to find more given the time and inputs they were given. Formal verification flips that logic: instead of searching for counterexamples, it builds a proof that no counterexample can exist within the defined scope. Historically, writing such proofs required a rare combination of software engineering and mathematical logic skills, and the proofs themselves could be many times larger and more complex than the original code.

What’s new here is that Claude performed this proof-writing work largely autonomously. Rather than assisting a human verification expert with suggestions, the model generated the formal proofs directly, a task that previously consumed years of dedicated specialist effort per project. Anthropic frames this as a capability shift: as models get better at this kind of rigorous, structured reasoning, formal verification becomes economically feasible for a far broader range of software than before.

Bugs found along the way

One notable side effect of the project is that the proof-writing process itself surfaced previously unknown bugs. According to Anthropic, Claude discovered defects in the code that had gone undetected despite trillions of test runs—a reminder that testing, no matter how extensive, samples only a fraction of a program’s possible behaviors, while formal verification attempts to reason about all of them within its defined scope.

What this means for developers

For working developers, the practical implications depend on how this capability matures. Anthropic is publishing a subset of the proofs, along with the RISC-V and OS semantics used, so that others can inspect and reuse them. Theorem, Anthropic’s collaborator on the project, is also offering to run the same verification pipeline on other open-source projects, which could let maintainers request proofs for their own libraries without building in-house formal methods expertise.

Caveats remain important. The proofs apply to specific, constrained conditions—a single-threaded static binary with a fixed memory budget on RISC-V under Linux—not to arbitrary deployment environments or multi-threaded code. This is not a claim that all bugs in these libraries have been eliminated, but rather that a specific, well-defined class of crashes and memory-safety violations cannot occur under the modeled conditions. Anthropic itself describes this as a step toward broader bug elimination rather than a complete solution.

Frequently asked questions

What is formal software verification?
It’s a method of mathematically proving that a program satisfies certain properties—such as never crashing or never accessing invalid memory—under a defined set of conditions, rather than just testing for bugs and hoping none remain.

Does this mean the verified libraries have zero bugs?
No. The proofs guarantee the absence of specific issues, like memory-safety errors and failed assertions, within defined constraints (certain input sizes, a single-threaded static binary, RISC-V and Linux). Bugs outside that scope could still exist.

Can other developers access these proofs or try this themselves?
Anthropic says it is publishing a subset of the proofs along with the underlying RISC-V and OS semantics, and its collaborator Theorem is offering to run the same verification pipeline on other open-source projects.

Source: LLMs are making formal software verification feasible at a much larger scale