Anthropic Uses Claude to Formally Verify 123 OSS-Fuzz Libraries at the RISC-V Assembly Level

What Anthropic and Theorem announced

Anthropic announced, in collaboration with the verification company Theorem, that Claude can write formal software proofs at a scale that was previously impractical. The team used Claude to prove security properties directly on compiled RISC-V assembly in more than 100 real-world open-source libraries — specifically, 239 fuzzing entry points across 123 OSS-Fuzz libraries. Anthropic describes the result this way: "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."

The property proved is narrower than "bug-free," and Anthropic is explicit about that. Claude proved that each covered program will always exit normally without triggering memory-safety errors or failing assertions, for every input less than 64 MB and every modeled Linux operating system response and memory layout. Those proofs assume the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU running Linux.

Key numbers from the OSS-Fuzz verification effort

239 fuzzing entry points proved, across 123 different OSS-Fuzz libraries.
Roughly 180 million lines of Rocq proof in total.
About 600,000 lines for a typical proof, covering binaries with a median length of 18,000 RISC-V instructions.
A few weeks of work to produce the proofs.

Formal verification has historically been expensive in expert time rather than compute. Anthropic cites seL4, the verified operating system kernel, which took two person-years to implement but 20 person-years to formally verify. That cost profile is why verification has been confined to mission-critical code such as Airbus avionics. The claim in this work is that LLM-generated proofs change that calculus.

How fuzz tests are converted into formal specifications

The core methodological move is to avoid writing specifications by hand. For most programs, a comprehensive and unambiguous spec is the hard part — as Anthropic asks, what would it mean for a text editor or a web browser to be "correct"? Instead, the team encodes the rule "this existing test suite always passes" as a formal spec over the compiled RISC-V instructions, using a general model of what it means to execute any RISC-V-compiled binary on Linux.

Concretely, the pipeline works in four stages:

A library and its existing fuzz test are compiled to a RISC-V executable. OSS-Fuzz automatically instruments C and C++ programs with AddressSanitizer (ASan), which makes improper memory accesses crash.
Theorem's formal RISC-V instruction and Linux process semantics translate the machine code into a mathematical model.
Claude writes a Rocq proof that the generated specification holds.
The Rocq proof checker mechanically verifies the proof against the specification.

The spec states that the fuzz test will not crash for any input under 64 MB. If the proof holds, fuzzing that entry point can no longer find anything. Proving "no crash" while ASan is linked in also establishes memory safety for the covered paths, because ASan converts out-of-bounds accesses into crashes.

What developers must actually trust

Anthropic argues that virtually none of the generated proof code needs human review, because the Rocq proof checker enforces correctness of the proof against the spec. The trusted artifacts that remain are small and enumerable:

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

Anthropic states the consequence plainly: "This doesn't mean these libraries contain no bugs." Remaining bugs either live inside those trusted components or fall outside the scope of the proof. Hardening those components is not trivial, but Anthropic argues it is far more tractable than auditing every line covered by the proofs — and, unlike the code, the trusted base does not grow as more projects are verified.

Bugs found that years of fuzzing missed

Attempting the proofs surfaced hundreds of bugs, and Claude was allowed to patch them autonomously: it fixed the code, the spec was regenerated from the patched code, and Claude then proved the new spec. This mattered because many of the bugs were outside the reach of conventional fuzzing, which typically mutates small inputs capped at about 1 MB and relies on coverage guidance.

Specific examples reported by Anthropic:

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 needed deeply nested input.
A logic bug that never crashes: while proving memory safety, Claude noticed that a feature for restricting which files an application can load is not always enforced.

Anthropic summarizes the point of this: even when the ultimate goal — a completed no-crash proof — is not reached, the attempt itself yields real bugs that need fixing.

Proving properties beyond memory safety

Proving a fuzz test never crashes is stronger than it sounds, because real-world fuzz tests frequently encode high-level properties: encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to a reference implementation. A fuzz test for the LZO compression algorithm, for example, asserts that compressing an input and then decompressing it returns the original. If the property fails, the program crashes, so proving the test never crashes is equivalent to proving the property itself.

Properties can also become necessary mid-proof without being stated by the developer. 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. That recursion depth is bounded by the maximum depth of a tree, so Claude had to prove on machine code that libc++'s red-black tree rebalancing algorithm keeps the tree depth logarithmically bounded.

Other formal verification case studies in the same report

Anthropic describes three additional experiments beyond the OSS-Fuzz pipeline.

zlib against RFC 1950. Claude wrote a formal spec of RFC 1950, the document defining the zlib compression file format, and then proved that the zlib implementation in the Linux kernel correctly implements that spec. The property was proved at the binary level, but on the x86-compiled binary rather than RISC-V, using Claude-generated and heavily tested formal semantics of the x86 instruction set. Anthropic repeated the process for half a dozen other widely used libraries and found minor, unexploitable bugs in corner cases that are being filed upstream. The two conclusions drawn: these extremely well-tested codebases are already almost fully correct, and end-to-end correctness properties about real existing codebases are provable.

A Python interpreter in Rust verified with Verus. Claude developed an interpreter for a large subset of Python in Rust and proved, using Verus, that it adheres to the CPython semantics outlined in an academic paper. Anthropic then tested adherence empirically with over 1.7 million randomly generated Python programs and found identical behavior to CPython in 99.95% of tests, with the remaining differences described as unsurprising known corner cases.

Security properties in critical applications. Verifying simple security properties of widely used software surfaced issues directly: in one application, a previously unknown logic bug that had been latent for more than a decade, and in a widely used PDF reader, as many security bugs found in one week as are typically reported in a year.

Cost, token efficiency, and proof reuse

Anthropic names cost as the main current limitation: proofs can take hundreds of millions of tokens to produce. Two trends are given as reasons to expect improvement.

First, newer models need fewer tokens. On 36 small verification tasks built 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 counted as proven when the first attempt finished. Anthropic expects the trend to continue as models are trained on long verification tasks.

Second, proofs can be reused. Proofs, like software, are recursively built from smaller proofs, and smaller proofs are more reusable. When agents worked in a shared workspace and copied each other's proofs, they needed 17% fewer tokens than agents working alone, and some agents succeeded after previously failing solo. Across the 36-task experiment, the shared-workspace cost was lower than the solo average in 30 of the 34 completed proofs, and agents working alone were unable to complete two of them.

The same effect appeared at scale in the OSS-Fuzz effort. Much of any proof concerns code every program contains, particularly C runtime and AddressSanitizer initialization, so unrelated programs end up with heavily overlapping proofs. Agent teams copied a finished proof and adapted it to their own program; in the released comparison for libcups, freerdp, and libzmq, the shared portions gained almost no new code.

Anthropic compares this to Mathlib, the shared library of formal mathematics in Lean, which grew to nearly 300,000 theorems contributed by over 700 people because each new proof builds on existing work. The company released a subset of the OSS-Fuzz proofs, withholding proofs that might reveal an unpatched bug.

Released artifacts and how to reproduce the work

Proofs: a subset is published at github.com/theorem-labs/oss-verify-proofs, including complete Rocq proofs for fuzz tests that did not require patching, plus specifications for fuzz tests that could not be proved.
Semantics: the RISC-V and Linux process semantics used as the trusted model are published at github.com/theorem-labs/rocq-linux-process-semantics.
Tooling: Theorem published a Claude skill to help developers onboard their own code, and is offering to run the same pipeline for other open-source projects.
Full appendix: a longer PDF appendix covers the additional case studies and an outside expert's assessment of the proofs.

The stated limitations of LLM-assisted formal verification

Anthropic devotes a section to why "formally verified" is not the same as "bug-free," and it identifies three distinct gaps.

The real machine does something the model does not describe. The proofs concern single-threaded, static RISC-V binaries linked against musl libc, while most users run these libraries on x86 or ARM and link dynamically against glibc. Closing that gap would require system models that more closely resemble deployed systems — for example, accurate semantics for x86.

The claim may not cover everything that matters. ASan does not detect all memory safety bugs, and not every entry point in each library was verified. Even verifying all entry points would not cover the whole library, particularly if there is dead code. Real programs can also misuse a library and cause memory corruption in the caller; closing that gap would require specifying what callers must do for each public function and requiring callers to adhere to it.

The spec may not match reality. A proof checker cannot tell you whether the spec corresponds to the real world. Anthropic writes: "Claude can write a proof showing that a compiled program's behavior satisfies the requirements of a formal spec (which is verified by an external proof checker). However, a proof checker can't tell you whether your spec matches reality." When bugs appear in verified code, it is because the spec or the assumed machine semantics diverge from reality — which at least tells you where to look.

What the Hacker News discussion added

The most reprinted critique in the discussion was that verification is only as good as its specification. One commenter summarized the ladder as vision, blueprint, and inspection: "This research makes the inspection close to perfect. But an inspection only checks the blueprint, not our vision, so a house built from the wrong blueprint can still pass a perfect inspection." A related comment asked how anyone can be sure the model faithfully represents the program being verified — "Couldn't it very well be that you proved something that wasn't actually your program?" — and another put it more bluntly: "Imagine having a formal spec for reality!"

A second theme was that the standard verification-versus-validation distinction still applies. One commenter framed it in IEEE terms: verification asks "Are we building the product right?" while validation asks "Are we building the right product?" — "You can write mathematically flawless code that highly efficiently solves the wrong problem."

A third theme was a predicted capability wall. One commenter quoted the report's own appendix, which asks whether agents can scale a verbose proof style to more complex programs and notes that "experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style." The same commenter argued that formal verification is a useful litmus test for LLM reasoning precisely because these systems are not necessarily on distribution for the model, lending credibility to a "convex hull" hypothesis that LLMs will stall just beyond the frontier of human-produced mathematics.

Practitioners in the thread reported their own successes. One said they had built a compiler translating both Rust and C into Lean and had an LLM prove behavioral equivalence, covering roughly 12% of the code — about 70,000 lines of C — for single-threaded execution, finding very minor differences such as floating-point behavior varying across platforms. Another described an agent opening a PR that speeds up a function with SIMD or CUDA and merging it confidently "because the PR has a Rocq proof that it's behaviorally equivalent to the original implementation." A third reported using Codex to build an Alloy model of an authorization system and then red-teaming the server for hours without producing a privilege escalation.

Skepticism also focused on organizational incentives rather than technical limits. One commenter doubted adoption would follow: "since our adoption of LLMs in software so far has mostly been to throw out best practices, I am skeptical that it will lead us to expanded verification," comparing the promise to executives predicting shorter work weeks. Another warned that laziness is the real risk — skipping code review and vibe-coding formal verification will still cause trouble, and "perfect is the enemy of good."

Several commenters raised the labor impact directly, and one asked whether the report's authors had considered that the proofs matched the Lean analogy of a plausible paper that does not match its formal artifact, referring to earlier OpenAI Lean work. Others asked for more detail on the workflow from code to proof, and at least one noted that Claude does not reach for formal verification unless instructed to.

Why this matters for how software gets built

Anthropic's conclusion is a trajectory claim rather than a finished-product claim: formal verification, historically practical only for bespoke expert-crafted guarantees in the most safety-critical code, will become as practical for most production software as fuzzing is today, moving from bolted-on to built-in alongside language design and development workflow changes. The company explicitly encourages developers who tried formal verification with less capable models and found it did not work to try again.

The report also outlines a strategy for the existing software base: verify at the binary level with generic specs so codebases do not need rewriting in another language, and reuse proofs at package granularity so each dependency is verified once. Dependencies follow a power law, so proving a small set of shared libraries — Theorem's roadmap names glibc, OpenSSL, and cURL within the Nix ecosystem — would make a large swath of software feasible to verify.