Claude and Theorem proved 239 entry points in 123 OSS-Fuzz libraries never crash on inputs under 64 MB
The proofs total about 180 million lines of Rocq and turned up hundreds of bugs that fuzzing missed
It targets compiled C, C++ and Rust at hundreds of millions of tokens per proof, not a Next.js app
A one-hour fast-check property catches the two classic signed-link bugs on its first generated input
On October 22 Anthropic published a research post with a number I read twice: about 180 million lines of machine-checked proof, written by Claude. Formal verification at that scale has never been done by hand. I build web apps, not compilers, so I read it with one question. Should I be using this? Not directly, it turns out. But the idea underneath it has a one-hour version that any app developer can use this afternoon, and I'll show it on a piece of code almost every shop has: a signed download link.
What Claude and Theorem Actually Proved
The project, run with a company called Theorem, started from fuzz tests in OSS-Fuzz, Google's continuous fuzzing program for open-source libraries. Each fuzz test became a formal claim: this test won't crash for any input smaller than 64 MB. Not "didn't crash in a billion runs". Any input at all.
Claude wrote proofs of that claim for 239 entry points across 123 libraries. They're written in Rocq, the proof assistant formerly called Coq, and the Rocq checker verifies every step, so nobody has to trust the model. A typical proof runs about 600,000 lines for a binary with a median of 18,000 RISC-V instructions. All of it adds up to roughly 180 million lines.
The good part happens when a proof refuses to go through. Usually that means the claim is false, which means there's a bug. Attempting the proofs surfaced hundreds of them. One counter underflow only triggered on inputs of around 20 MB with one rare, specific layout, the kind of input a fuzzer almost never stumbles into. Another was a rediscovery of a libexpat CVE that needed deeply nested input.
The post covers other experiments too:
The zlib implementation in the Linux kernel, proven to implement a formal spec of RFC 1950.
A Python interpreter written in Rust and checked with Verus against CPython semantics from an academic paper. In testing it matched CPython on 99.95% of 1.7 million randomly generated programs.
A widely used PDF reader, where one week of verification work found as many security bugs as usually get reported in a year.
The authors are blunt about limits. "Formally verified" does not mean "bug-free." The proofs assume single-threaded static binaries, a fixed memory budget, RISC-V and Linux, with musl rather than glibc. The trusted base includes the Rocq checker and the machine models. And a single proof can take hundreds of millions of tokens.
Why the Formal Verification Results Matter Even If You Never Write a Proof
Some context on why this is a big deal. The seL4 microkernel, the best-known verified kernel, took two person-years to implement and many times that to verify by hand. Proof effort used to be measured in careers.
Now it's measured in tokens, and tokens get cheaper. On a set of 36 small verification tasks, Opus 5.5 proved half of them with about 40% fewer tokens than Opus 5. Agents sharing one proof workspace needed 17% fewer tokens than agents working alone.
The first winners are the libraries everything depends on. Dependencies follow a power law: a few hundred libraries (compression, XML and image parsers, crypto) sit under almost every app ever shipped. Verify those and most of the software world inherits the guarantee without its authors lifting a finger. I find that more exciting than the 180 million figure.
That includes any web stack. A Next.js app runs on Node, which sits on libraries exactly like these. Bugs those proofs find get patched upstream and reach you through your next dependency update. So the practical takeaway for an app developer is unglamorous: keep dependencies current. Run npm audit or bun audit on a schedule. Most fixes it reports are in-range lockfile updates that take a minute and a test run. That's the route verified upstream code takes to reach you.
Theorem released a subset of the proofs, the RISC-V and Linux process semantics, and a Claude skill for adding projects to the pipeline. They're also offering to run it on other open-source projects. If you maintain a C or Rust library with fuzz tests, that offer is worth a look.
Why I'm Not Running It on My Own Code
I looked at it seriously for my own repos and decided against it.
The pipeline proves properties of compiled C, C++ and Rust binaries that already have fuzz harnesses. My code is TypeScript, Shopify Liquid, Swift and some Python scripts. None of it compiles to the static RISC-V binaries the semantics model.
Cost rules it out on its own. Hundreds of millions of tokens per proof is research money. I run a hard rule that paid model calls only come from live products with a budget cap per run, and a proof campaign for a download page doesn't pass that bar.
There's a scope question too. Most incidents in a small stack aren't crashes. They're a hosting setting nobody checked, a credential that outlived its purpose, a runtime lagging behind a security release. A proof of crash-freedom covers none of that. I wrote up the runtime side of this month in eMudhra CA Break: Patch List for 6 Runtimes.
The 1-Hour Version: Property Tests on a Signed Link
The idea underneath formal verification still works at small scale: write down a property that must hold for every input, then attack it. Property-based testing does the attacking with generated inputs instead of proofs. It costs no tokens and runs in milliseconds. I use fast-check with Vitest or Node's built-in test runner.
Here's a very common shape for verifying a signed download link. It looks fine in review:
const enc = new TextEncoder();
function verifyLink(orderId: string, product: string, token: string) {
const expected = hmac(secret, `${orderId}:${product}`);
return token.length === expected.length &&
timingSafeEqual(enc.encode(token), enc.encode(expected));
}
It has two bugs. Write two properties and fast-check finds both on the first generated input.
Property one: a token opens only the order and product it was signed for.
fc.assert(
fc.property(orderId, product, anyText, anyText, (o, p, o2, p2) => {
fc.pre(o2 !== o || p2 !== p);
return !verifyLink(o2, p2, sign(o, p));
}),
);
It fails with the counterexample ["0", "a", "a"]. A link signed for order 0 and product a:a also verifies for order 0:a and product a, because both join to the same text. The fix is to refuse the delimiter inside either field, or to encode the fields unambiguously.
Property two: verification never throws, whatever the URL contains. It fails too. A 64-character token made of non-ASCII characters passes the string length check, then timingSafeEqual throws because the byte lengths differ, and the route answers 500 instead of 403. The fix is to compare byte lengths.
One practical tip for that second property: fast-check's binary string unit mostly generates characters outside the Basic Multilingual Plane, so the strings come out 128 UTF-16 units long and never reach the comparison. Generate exactly 64 BMP characters instead. More generally, run every new property against code you know is broken and watch it fail once. A property that can't fail proves nothing.
Good properties for a link check: a fresh link works for its whole validity window and stops right after, old link formats keep working, random tokens and tokens signed with another secret never verify. For an encryption helper: decrypt after encrypt returns the original for any text, and flipping any single bit makes decryption throw.
If you're choosing a runner, Bun's Test Runner Replaced Vitest in My New Projects compares the options I use. For Anthropic's other security tooling, see Claude Security: Anthropic's New Vulnerability Scanner.
Bottom Line
The Anthropic and Theorem results are real: 239 entry points proven crash-free, about 180 million lines of Rocq, hundreds of bugs found along the way. They target the libraries underneath everyone's stack, and app developers collect the benefit by keeping dependencies updated. For your own app code, take the habit and leave the tooling: write down what must always be true, then go looking for the input that breaks it. Two properties on a signed-link check take under an hour and catch both classic mistakes in that shape of code.
If you use Claude Code, this is the test I'd have it write for every function that touches money, auth or user data. My Claude Blueprint is the setup I run that from. Which function in your codebase would you least like to see a counterexample for?
This article contains affiliate links. If you sign up through them, I may earn a small commission at no extra cost to you. (Ad)
Top comments (0)