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

What it is

Anthropic and Theorem used Claude to turn OSS-Fuzz fuzz tests into formal specs over compiled RISC-V binaries, then prove them in Rocq. The spec says the entry point never crashes, including on ASan-detected memory errors, for any input under 64 MB. A typical proof runs about 600,000 lines, against binaries with a median of 18,000 RISC-V instructions. Where Claude found a bug, it patched the code, the spec was regenerated, and it proved the new spec.

How it works

• The spec is "this fuzz test always passes", stated over a general model of executing a RISC-V binary on Linux. No hand-written spec is needed.
• Fuzz tests that assert round trips or other properties are covered too. An LZO fuzz test that checks compress-then-decompress returns the original is proved as a correctness property. For cpp-httplib, Claude had to prove on machine code that libc++'s red-black tree rebalancing keeps depth logarithmic, to rule out stack overflow in the std::set destructor.
• Bugs the proving process surfaced that fuzzers would likely miss:
• A counter underflow in a decompressor leading to an out-of-bounds write, only on inputs of about 20 MB with one rare layout.
• An out-of-bounds read in an image decoder needing a 64 MB input and over 2 GB of memory.
• An out-of-bounds read needing a particular call sequence across two handles to the same file.
• CVE-2026-56132 in libexpat, rediscovered, which needs deeply nested input.
• A logic bug where a feature restricting which files an application can load is not always enforced.

Preconditions / Affected

The guarantees hold only for single-threaded static binaries with a fixed memory budget, on RISC-V, under Theorem's Linux process model, linked against musl libc. Most deployments run x86 or ARM with dynamically linked glibc, so the proofs do not directly transfer.

What to do

• To check the work, the trusted base is small: the RISC-V and Linux process models, the exact theorem statements, and the Rocq checker. The proof text itself need not be reviewed.
• Anthropic is publishing the trusted components not already public, the full proofs for fuzz tests that needed no patching, and specs for fuzz tests it could not prove. Proofs that could reveal an unpatched bug are withheld.
• Theorem offers to run the same pipeline on other open-source projects and is publishing a Claude skill for verifying your own code.
• Even a failed proof attempt is useful, since the attempt itself surfaced hundreds of bugs.

Caveats

• "Formally verified" does not mean bug-free. Remaining bugs can sit in the trusted models or outside the proved claim.
• ASan does not catch all memory-safety bugs. Not every entry point in each library was verified, so dead code and uncovered functions are outside the proof. Callers that misuse the library can still corrupt memory.
• Cost is high: proofs can take hundreds of millions of tokens. On 36 small OSS-Fuzz verification tasks, Opus 5.5 solved half with about 40% fewer tokens than Opus 5. Agents sharing a workspace of proofs used 17% fewer tokens than agents working alone.
• Side experiments are less rigorous. A Claude-written Python interpreter in Rust, verified with Verus, matched CPython on 99.95% of 1.7 million random programs. The zlib proof against RFC 1950 used Claude-generated x86 semantics, and the page reports only minor unexploitable bugs there. The PDF reader and the decade-old logic bug are described without naming the software.