Anthropic's LLM Formal Verification: Claude Proves No-Crash Properties in 123 OSS-Fuzz Libraries at the RISC-V Assembly Level

Anthropic and its collaborator Theorem report that Claude autonomously proved no-crash security properties for 123 real-world open-source libraries, working directly on compiled RISC-V assembly rather than on source code. Anthropic calls it the first large-scale effort to apply AI-driven formal verification to production software at the assembly code level, and says the proofs also surfaced bugs that years of fuzzing had missed.

What was announced

The core claim is that LLM-assisted formal verification has crossed a practicality threshold. Instead of relying only on fuzzing, which searches for crashes probabilistically, Claude produced mathematical proofs that certain compiled programs can never crash on any input within a defined bound.

Concretely, Anthropic reports that Claude proved useful security properties at the RISC-V assembly level in over 100 real-world open-source libraries. Across that effort, Claude completed proofs for 239 entry points spanning 123 libraries from Google's OSS-Fuzz initiative. The work was done in collaboration with Theorem, which supplied the RISC-V instruction and Linux process semantics used to translate machine code into a mathematical model.

Anthropic frames the motivation starkly: the Linux kernel, one of the most heavily tested pieces of software in existence, recently had over 1,000 vulnerabilities disclosed, and frontier models are increasingly capable of chaining seemingly benign bugs into critical exploits. If LLMs can find bugs at scale, the argument goes, defenders need techniques that can prove their absence rather than only test for it.

Using Claude, we proved security properties at the assembly code level (RISC-V) in over 100 real-world open-source software libraries. To our knowledge, this represents the first large-scale effort to use AI to apply formal verification to production software at the assembly code level.

How the pipeline turns fuzz tests into proofs

The pipeline reuses work developers have already done. OSS-Fuzz projects contain thousands of developer-authored entry points that crash the program when a property is violated, such as a failed assertion or an improper memory access detected by AddressSanitizer. Those entry points, plus the existing fuzz tests, are compiled into a RISC-V executable.

That executable, combined with Theorem's RISC-V and Linux semantics and the desired no-crash property, mechanically yields a specification that a proof must satisfy. Claude then writes the proof, and the Rocq proof checker verifies it against that specification. If the proof attempt fails, the failure points at a real bug; Claude patches the code, the specification is regenerated from the patched code, and the cycle repeats.

The exact property proved is narrow but meaningful: these programs will always exit normally without triggering memory-safety errors or failing assertions, for every input less than 64 MB, and for every modeled Linux OS response and memory layout.

The proofs hold under stated assumptions: that the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU running Linux. Anthropic notes that expanding scope would involve standardizing semantics for more assembly architectures and other operating system processes.

Scale of the proof effort

The numbers are the headline evidence that this is a different regime from hand-written verification.

• 239 entry points proved across 123 OSS-Fuzz libraries
• Roughly 180 million lines of Rocq proof produced in total
• A typical proof runs about 600,000 lines
• Median binary size covered by a proof: about 18,000 RISC-V instructions
• Input bound: every input less than 64 MB
• Timeline: a span of a few weeks

The historical comparison Anthropic draws is the seL4 operating system kernel, which took two person-years to implement but 20 person-years to formally verify. That ratio is why formal verification has been confined to mission-critical domains such as Airbus's avionics code.

What developers still have to trust

Almost none of the 180 million lines of proof code needs manual review, because the Rocq proof checker validates it. Anthropic lists exactly three artifacts that a developer must trust:

1. The formal models of RISC-V and of Linux processes
2. The exact theorem statements that were proved
3. The Rocq proof checker itself

This is the key structural argument. The trusted computing base does not grow with the number of projects verified. Anthropic explicitly warns that this does not mean the libraries contain no bugs. It means any remaining bug either lives inside those trusted artifacts or falls outside the scope of the proof. Hardening Rocq, the RISC-V semantics, and the Linux semantics is real work, but it is a bounded task rather than a per-project burden.

Bugs Claude found while writing proofs

Attempting the proofs turned out to be a bug-finding process in its own right. Anthropic reports that the effort discovered hundreds of bugs, and that many of them are ones a fuzzer would be unlikely ever to find. The reason is mechanical: fuzzers mutate small inputs, typically capped at 1 MB, and rely on code coverage to guide the search.

Specific examples Anthropic describes:

• A counter underflow in a library's copy of a decompressor that led to an out-of-bounds write, reachable only on inputs of around 20 MB with one rare, specific layout.
• An out-of-bounds read in an image decoder that required a 64 MB input and over 2 GB of memory.
• An out-of-bounds read in another library that required a particular sequence of calls across two handles to the same file.
• A rediscovery of CVE-2026-56132 in libexpat, which required deeply nested input.
• A pure logic bug with no crash at all: while proving one library memory-safe, Claude noticed that a feature for restricting which files an application can load is not always enforced.

To avoid stopping for a human each time a bug appeared, Anthropic let Claude patch the bugs it found as part of the same loop.

Proving more than memory safety

Proving that a fuzz test never crashes is stronger than it sounds, because real fuzz tests encode high-level properties rather than only memory checks. Anthropic lists encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, and equivalence to reference implementations as common examples. A fuzz test for the LZO compression algorithm, for instance, asserts that compressing and then decompressing an input returns the original; because failure crashes the program, proving the test never crashes is equivalent to proving the property itself.

Sometimes the required obligations go further than the developer intended. To finish the OSS-Fuzz proof for cpp-httplib, Claude had to rule out a stack overflow caused by excessive recursion in the std::set destructor. Because that recursion depth is bounded by the maximum depth of a tree, Claude had to prove at the machine-code level that libc++'s red-black tree rebalancing algorithm keeps the tree's depth logarithmically bounded.

Other formal verification case studies

Anthropic describes several additional experiments beyond the OSS-Fuzz fuzz-test-to-proof pipeline.

zlib and RFC 1950. Claude wrote a formal specification of RFC 1950, the document defining the zlib compression file format, then proved that the zlib implementation in the Linux kernel correctly implements that spec. Unlike the RISC-V work, this proof was performed directly on the x86-compiled binary using Claude-generated and heavily tested formal semantics of the x86 ISA. The process was repeated for half a dozen other widely used libraries, and turned up minor, unexploitable bugs in corner cases that are in the process of being filed upstream. Anthropic draws two conclusions: these extremely well-tested codebases are already almost fully correct, and end-to-end correctness properties can be proved about real existing codebases.

A Python interpreter in Rust. Claude developed an interpreter for a large subset of Python in Rust and proved, using the Verus verification tool, that it adheres to CPython semantics as outlined in an academic paper. Empirical testing on over 1.7 million randomly generated Python programs found identical behavior to CPython in 99.95% of tests, with the remaining differences being unsurprising known corner cases.

Critical applications. Formal verification attempts of simple security properties surfaced issues in several widely used and critical applications. In one case, Claude found a previously unknown logic bug that had been latent for more than a decade. During an effort to verify a widely used PDF reader, Anthropic reports finding as many security bugs in one week as are typically reported in a year.

Cost: token usage and why it should fall

Anthropic identifies token cost as a key limitation. Proofs can take hundreds of millions of tokens to produce, and cost-efficiency matters if these methods are to reach the entire software ecosystem. Two measured trends suggest the cost will drop.

The first is model improvement. Anthropic built 36 small verification tasks from real OSS-Fuzz code. Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. Each task received three independent single-agent attempts at a 5M-token budget, and counts as proven when the first attempt finishes.

The second is proof reuse. When agents were given a shared workspace where they could copy each other's proofs, they needed 17% fewer tokens than when working alone, and some agents succeeded on tasks where a solo attempt had previously failed.

The same effect appeared at scale in the OSS-Fuzz effort. Most of a proof concerns code that every program contains, particularly initialization of the C runtime and AddressSanitizer, so very different programs end up with significantly overlapping proofs. Agent teams copied another team's finished proof and adapted it. In the published comparison of libcups, freerdp, and libzmq, each proof is broken down by how much was kept identical, lightly edited, edited more, or newly written, and the shared parts gained almost no new code. Of the 36 shared-workspace proofs, 34 were completed, and 30 of those cost less than the average solo agent attempt.

Anthropic compares this dynamic to Mathlib, the shared library of formal mathematics in Lean, which grew to nearly 300,000 theorems submitted by over 700 contributors because each new proof builds on existing work.

Limitations Anthropic acknowledges

The post is explicit that formal verification does not deliver the guarantee people assume.

"Formally verified" does not mean "bug-free." A proof checker can show that a program satisfies a spec, but it cannot tell you whether the spec matches reality. When bugs appear in verified code, the spec or the assumed machine semantics differs from reality. Anthropic argues this is still useful, because it tells you where to look for the remaining bugs.

The real machine does something the model doesn't describe. The proofs cover single-threaded, static RISC-V binaries linked against musl libc. Most people run these libraries on x86 or ARM with dynamic linking against glibc. Closing this gap would require system models that more closely resemble deployed systems, for example generating accurate semantics for x86.

The claim may not cover everything we care about. ASan does not detect all memory safety bugs, and not all entry points for each library were verified. Verifying all entry points still would not cover the whole library, especially where dead code exists. Real programs can also misuse a library in ways that corrupt memory in the caller; closing that gap would require specifying what callers must do for each public function and having callers strictly adhere to it.

What was released

Anthropic and Theorem published several artifacts alongside the post:

• A subset of the proofs, at github.com/theorem-labs/oss-verify-proofs, including Claude's complete Rocq proofs for fuzz tests that did not require patching, plus specifications for fuzz tests that could not be proved.
• The RISC-V and OS semantics, at github.com/theorem-labs/rocq-linux-process-semantics.
• A Claude skill, at github.com/theorem-labs/oss-verify, to help developers start verifying their own code.
• An offer from Theorem to run the same pipeline for other open-source projects.

Anthropic deliberately withheld proofs that might reveal an unpatched bug in open-source software, and invites independent verification of what was published.

Why this matters

The strategic argument is that as LLMs get better at finding and chaining vulnerabilities, testing alone becomes an insufficient defense. Formal verification offers a guarantee rather than a probability, and its historical blocker was the cost of writing proofs, not their value.

Anthropic also argues that the unit economics favor packages rather than programs. Proof reuse works at package-level granularity, so each dependency only needs to be verified once, and dependencies follow a power law: proving a small set of shared libraries makes a huge swath of downstream software feasible to prove. Theorem's roadmap for verifying the entire Nix ecosystem, which includes critical infrastructure such as glibc, OpenSSL, and cURL, is presented as the immediate large-scale application.

The closing prediction is that formal verification, historically practical only for bespoke expert-crafted guarantees in the most safety-critical code, will become as practical as fuzzing is today for almost all production software, moving from bolted-on to built-in. Anthropic explicitly encourages developers who previously tried formal verification with less capable models and found it did not work to try again.