Claude proved 123 open-source libraries can't crash on RISC-V

Two days after two PHP bugs put a slice of the internet into an unscheduled maintenance window, Anthropic published the closest thing to an antidote anyone has shipped: Claude wrote formal proofs that 123 open-source libraries cannot crash, at the assembly level, for any input up to 64 MB. The qualifier at the end of that sentence is where the real story is.

What they actually proved

Anthropic worked with Theorem, a verification startup, and pointed Claude at Google's OSS-Fuzz corpus — the continuous fuzzing programme that has been hammering open-source C and C++ since 2016. Fuzzing works by throwing semi-random inputs at an entry point until something crashes. Claude's job was to turn each test into a theorem: for every input under 64 MB, this entry point exits normally, with no memory-safety error and no failed assertion.

It managed that for 239 entry points across 123 libraries, in a few weeks. The proofs run to roughly 180 million lines of Rocq, a typical one about 600,000 lines long covering a binary with a median length of 18,000 RISC-V instructions. Along the way Claude found bugs that fuzzing had missed despite trillions of runs, patched them, and then proved the patched code crash-free, Anthropic says in its write-up. A subset of the proofs and the machine semantics underneath them are published on GitHub, so the checking does not depend on trusting the lab.

That last part is the difference between a demo and a tool. A proof of this kind is not an argument a reader has to believe; it is a file a checker either accepts or rejects. Anthropic's own framing is that almost none of the 180 million lines need human review — you need to trust four things instead: the RISC-V model, the Linux process model, the exact theorem statements, and the Rocq checker itself. Everything else is mechanical.

The ratio that changed

Formal verification was never impossible, just unaffordable. The canonical example is seL4, the microkernel that took two person-years to write and twenty to verify, by the seL4 team's own accounting. That 10:1 overhead is why verification has lived in avionics and payment switches and nowhere else.

The economics invert when a model writes the proof and a machine checks it. The expensive input was never compute; it was the small number of people who can write Rocq at all. Claude is not good at proofs in the abstract — it is good at grinding through millions of lines toward a goal someone else defined, which is precisely the shape of this task. Anthropic's honest caveat is that the goal was cheap to define here: they reused fuzz tests as specifications, because "this test suite always passes" is a property a project already wrote down. Libraries without good fuzz harnesses do not get this for free.

The other thing that changed is the size of the trusted base. Verifying a library used to mean trusting the proof, the prover, the compiler and the specification — an argument that got weaker with every layer. Here the trusted components are small, fixed, and shared across all 123 libraries, so the cost of verifying library 124 is mostly the cost of running the pipeline again. Theorem is already selling that as a service and publishing a Claude skill for adding a project. That is the commercial tell: the bottleneck moved from expertise to throughput.

The binary they proved isn't the one you run

Anthropic's assumptions are narrow and they say so. The proofs cover single-threaded, statically linked RISC-V binaries with a fixed memory budget, running against musl libc on a modelled Linux. Almost nobody deploys that. Real systems are x86 or ARM, dynamically linked against glibc, often threaded, and the model of the operating system is itself an approximation. Claude proving your code crash-free on a machine you do not operate is a real guarantee about a hypothetical.

The limitations list is worth reading in full, because it is unusually candid: AddressSanitizer does not detect every memory-safety bug, not every entry point in every library was verified, and a proof about a library says nothing about a caller that misuses it and corrupts its own memory.

Then there is the category problem. Crash-freedom at a fuzz entry point is not "this input is trusted" and not "this authorisation check is correct". This week's PHP vulnerabilities sat in the interpreter's handling of uploaded data — a logic failure about where attacker-controlled bytes end up, not a memory-safety failure a checker would catch. We traced what those two bugs did to the web yesterday; nothing in a crash-freedom proof speaks to that class of mistake. Anthropic's own line is the right one: formally verified does not mean bug-free, it means the remaining bugs are inside a much smaller box.

Who wins

Theorem gets the reference customer and a funnel of open-source projects to convert into paying ones. Anthropic gets the strongest argument yet that its models do something other than autocomplete — and one that pairs awkwardly well with its own exploit research, which is the same capability pointed the other way. OSS-Fuzz gets proofs sitting on top of its corpus, which is a better outcome for Google than being replaced by one. Maintainers get bug reports they did not have, which is free until it becomes a backlog.

The losers are the marketing claims. "AI found every bug" was already an overstatement; "formally verified" is about to become one too, printed on slides next to a proof that assumes a CPU, an operating system and a threading model the customer does not use. The useful habit for anyone reading those slides is to ask what the trusted base is and what the specification said. If the answer is "we ran a checker and it passed", the next question is what the checker was told to check.

What to watch

x86 semantics, which Anthropic names as the next step and which is the gate for anything deployed in production. Whether a major library accepts these proofs into continuous integration, because a proof that goes stale with the next commit is a screenshot, not a guarantee. And whether anyone points the pipeline at an interpreter rather than a library — PHP, OpenSSL, a browser engine — where the interesting bugs are design decisions rather than memory accesses. That is the test the tools have not yet passed.

If a proof only covers the machine you don't run, is it a security guarantee or a press release? Write to us via our contact page.