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

What it claims

Anthropic and Theorem turned OSS-Fuzz fuzz harnesses into formal specs and had Claude prove them in Rocq. The spec states that the harness, compiled to RISC-V, exits normally with no AddressSanitizer error or failed assertion for every input under 64 MB. It must hold for every modeled Linux OS response and memory layout. A typical proof is about 600,000 lines and covers a binary with a median of 18,000 RISC-V instructions. The work took a few weeks. Because many harnesses assert properties such as compress-then-decompress roundtripping (the LZO example), a crash-freedom proof also proves that property. One cpp-httplib proof required showing, on machine code, that libc++'s red-black tree keeps logarithmic depth, which rules out stack overflow in the std::set destructor.

How it works

Theorem's RISC-V instruction semantics and Linux process semantics translate each binary into a mathematical model. When a proof attempt fails, the failure points at a candidate bug. Claude patches the code, the spec is regenerated from the patched binary, and the proof restarts, with no human in the loop.

flowchart TD
  A[OSS-Fuzz harness + ASan] --> B[Compile to RISC-V]
  B --> C[Spec: no crash, input < 64 MB]
  C --> D{Claude proof in Rocq}
  D -- checks --> E[Proved entry point]
  D -- stuck on bug --> F[Claude patches code]
  F --> B

The trusted base is only three things: the RISC-V and Linux models, the exact theorem statements, and the Rocq checker. The 180 million proof lines need no manual review.

Evidence

The bugs found include several that fuzzers, which usually cap inputs near 1 MB, are unlikely to reach:

• a counter underflow causing an out-of-bounds write in a bundled decompressor, triggered only by a roughly 20 MB input with a rare layout;
• an out-of-bounds read in an image decoder that needs a 64 MB input and over 2 GB of memory;
• a rediscovery of CVE-2026-56132 in libexpat, which needs deeply nested input;
• a logic bug where a file-loading restriction is not always enforced.

Separate case studies:

• Claude wrote a formal spec of RFC 1950 (zlib) and proved that the Linux kernel's zlib implementation meets it, on the x86 binary, using x86 semantics that Claude generated. The same was done for half a dozen other libraries and found only minor, unexploitable bugs.
• A Rust interpreter for a Python subset was proved in Verus against an academic CPython semantics. It matched CPython on 99.95% of 1.7 million random programs.
• An attempt to verify a PDF reader found as many security bugs in one week as are usually reported in a year.

On cost, the 36-task benchmark built from OSS-Fuzz code is small. On half of those tasks, Opus 5.5 used about 40% fewer tokens than Opus 5. Agents that shared a proof workspace used 17% fewer tokens, and some succeeded where solo attempts had failed. Proofs overlap heavily because most of each proof covers C runtime and ASan initialization.

How to use it

The release includes:

• the non-public trusted components;
• complete proofs for harnesses that needed no patching;
• specs for harnesses that could not be proved.

Proofs that could reveal unpatched bugs are withheld. Theorem publishes a Claude skill for verifying your own code and offers to run the pipeline on other open-source projects. Theorem also has a roadmap for verifying the Nix ecosystem, including glibc, OpenSSL and cURL. The page gives no commands, licence or per-project cost.

Limits

• Proofs assume single-threaded, static RISC-V binaries linked against musl, with a fixed memory budget. Most deployments run on x86 or ARM with dynamic glibc.
• ASan does not catch all memory-safety bugs.
• Not every entry point of each library was verified. Even all entry points would not cover dead code or callers that misuse the API.
• Remaining bugs can sit in the RISC-V model, the Linux model, the theorem statements or Rocq.
• Producing a proof can take hundreds of millions of tokens.