Generated by Codex with GPT 5.6 Sol High

Techmeme surfaced Anthropic’s October 22 report, “LLMs are making formal software verification feasible at a much larger scale.” In collaboration with Theorem, Anthropic used Claude to turn existing fuzz tests into machine-checked proofs about compiled software. Across 123 open-source libraries, the system proved that 239 test entry points cannot crash for any input smaller than 64 MB under a defined execution model. That is narrower than proving the libraries bug-free, but far stronger than running even trillions of sampled tests.

The work matters because AI is changing both sides of software security. Models are becoming better at finding and combining vulnerabilities, yet the same ability to search through enormous technical spaces can make a historically expensive defensive technique practical. Formal verification does not ask whether many tests passed. It asks whether a stated property follows for every behavior allowed by a mathematical model.

Turning a fuzz test into a theorem

Fuzzing feeds a program large numbers of generated inputs and watches for crashes, assertion failures, or memory errors. It is one of the most effective ways to test parsers and low-level libraries, but it can never exhaust an infinite input space. Coverage also depends on the fuzzer reaching the right path. A bug triggered only by an unusually large input or a rare sequence of calls may survive years of continuous testing.

Anthropic and Theorem began with entry points from Google’s OSS-Fuzz project. These are developer-written harnesses whose crashes represent bugs the maintainers care about. The pipeline compiled each harness and its library into a statically linked RISC-V binary with AddressSanitizer, then represented the binary, a Linux process, and the desired no-crash property mathematically. Claude wrote a proof in Rocq, while Rocq’s small proof-checking kernel decided whether every step actually established the theorem.

This separates generation from judgment. Claude can produce hundreds of thousands of lines of proof without anyone trusting its prose or its confidence. The checker accepts only a derivation that satisfies the formal statement. Anthropic reports roughly 180 million lines of Rocq across the successful proofs, with a typical proof covering a binary of about 18,000 RISC-V instructions and running to about 600,000 lines.

The scale would be absurd if humans had to review those lines manually. They do not. The artifacts that require scrutiny are much smaller: the theorem being proved, the formal RISC-V and Linux semantics, and the Rocq checker. Concentrating trust in those components is the central advantage. Once the execution model and proof machinery are sound, the same foundation can check many programs without enlarging the trusted base for every new library.

Failed proofs become bug finders

A proof attempt is also a systematic search for counterexamples. When Claude could not establish the no-crash claim, it often found a real defect, patched it, regenerated the formal problem, and tried again. Anthropic says this process uncovered hundreds of bugs, including cases that ordinary fuzzing was unlikely to reach.

One decompressor contained a counter underflow that could produce an out-of-bounds write only with an input around 20 MB and a rare layout. Another image decoder required a 64 MB input and more than 2 GB of memory to expose an out-of-bounds read. The system also rediscovered a deeply nested libexpat vulnerability, found a bug requiring a particular sequence of operations through two handles to the same file, and identified logic errors that did not crash at all. In one separate project, a simple verification attempt exposed a logic bug that had remained latent for more than a decade.

The method can prove more than memory safety when a test encodes a richer invariant. If a compression harness asserts that decompressing a compressed input returns the original, proving that the harness never triggers its failure path establishes the round-trip property for the modeled inputs. While verifying cpp-httplib, Claude even had to prove at the machine-code level that libc++’s red-black-tree rebalancing keeps tree depth logarithmically bounded, because otherwise destruction could overflow the stack.

Anthropic reports additional experiments that point beyond fuzzing. Claude generated a formal specification for zlib from its RFC and proved that the Linux kernel’s x86 binary implements it. It also wrote a substantial Python interpreter in Rust, used Verus to prove correspondence with an academic account of CPython semantics, and matched CPython on 99.95% of 1.7 million randomly generated programs. These are distinct experiments rather than one universal verification system, but together they show that models can help with specifications, machine semantics, implementation, and proofs.

The guarantee is only as broad as the model

“Formally verified” does not mean “bug-free.” The headline result covers particular fuzz-test entry points, not every public function or every way an application might misuse a library. It rules out covered crashes for inputs below 64 MB under a single-threaded, static RISC-V Linux model with a fixed memory budget. Most deployed software instead runs on x86 or ARM, uses dynamic linking, relies on different C libraries, and executes concurrently. Any mismatch between the formal semantics and the real machine sits outside the guarantee.

AddressSanitizer also detects only certain classes of memory error. Dead code, caller mistakes, concurrency defects, side channels, incorrect requirements, and malicious behavior permitted by an incomplete specification can remain. A proof checker establishes that code satisfies the statement it was given; it cannot decide whether that statement captures what users actually need.

Allowing Claude to patch code creates another risk. An agent could make a theorem easy by deleting behavior or replacing the program with something that trivially does not crash. Anthropic says it penalized patches, rewarded minimal behavioral changes, logged them, and audited for this kind of reward hacking. Those controls are useful, but published proofs without the bug-revealing patches represent only a subset of the work, so independent reviewers cannot yet reproduce every claim.

Cost remains substantial. The proofs can consume hundreds of millions of tokens, although Anthropic’s small benchmark found that Opus 5.5 used about 40% fewer tokens than Opus 5 on tasks both could solve. Letting agents reuse one another’s work reduced token use by 17% in another experiment. That reuse may be decisive: common runtime, sanitizer, and library components recur across binaries, so one verified dependency can support many downstream proofs.

The credible near-term conclusion is not that all software can now be proven safe. It is that the economics of verification may have crossed an important threshold. Existing fuzz harnesses can supply useful specifications; models can generate enormous proof artifacts; and a conventional checker can validate them without trusting the model. That creates a practical path from “we tested many cases” toward “we proved this defined failure cannot occur”—provided developers remain precise about exactly what was modeled, what was proved, and what still lies outside the theorem.