The Fuzz Harness Was Already the Spec

On October 22 Anthropic’s Frontier Red Team and Theorem Labs published a report on formal verification at scale. The pipeline is short. Take an existing OSS-Fuzz harness and state the theorem “this harness never crashes on any input under 64 MB.” Compile the library to a static RISC-V binary linked against musl. Have Claude write a Rocq proof against a formal model of the RISC-V ISA and the Linux process, then let the Rocq kernel check it. In a few weeks this covered 239 entry points across 123 libraries and produced about 180 million lines of Rocq. A typical proof is around 600k lines for a binary with a median of 18k instructions. Along the way it found bugs that had “eluded detection for years, despite trillions of test runs”: CVE-2026-56132 in libexpat, which needs deeply nested input; a decompressor counter underflow that only fires around 20 MB; and an image-decoder out-of-bounds read that needs a 64 MB input and more than 2 GB of memory. The authors claim formal verification “will soon be as practical as fuzzing is today for almost all production software.” I want to make the strongest case for that claim before pushing it further.

The checker was never the expensive part of formal methods. Two things were: writing specifications and writing proofs. This pipeline doesn’t write new specifications. A fuzz harness is a spec that someone already wrote, still maintains, and runs in CI, and wrapping it in “always passes” turns it into a theorem. The proofs are paid for in tokens. Nobody reads 600k lines of Rocq; what you trust is the ISA and process model, the one-line theorem statement, and the kernel. The report is upfront about what’s left out: single-threaded RISC-V/musl binaries when production runs x86/glibc, memory-safety bugs that ASan misses, misuse by callers, and proofs that can cost “hundreds of millions of tokens.” Most of the pushback in the Hacker News thread is about the spec, not the proof. A spec should be readable by a human. Someone has to check a spec the model wrote itself. Concurrency, “the source of all the hard stuff,” was avoided. All fair points, but none of them touches the narrower claim, which is crash-freedom proved against harnesses humans already wrote.

Taken at its word, the claim leads somewhere else as well. Once a mechanical checker decides success, comparing models gets very simple. There’s no judge, no rubric, no rater disagreement and no position bias. Rocq either says QED or it doesn’t, so the only thing left to compare is tokens-to-QED. The report’s small benchmark has this shape: on 36 verification tasks, Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. When each proof costs hundreds of millions of tokens, a 40% gap decides whether the pipeline can run at all. As rough arithmetic, 239 proofs at 200M tokens each comes to about 48B tokens, and 40% of that is about 19B. The second extension is that cost depends on what has already been proved. With shared proofs, agents “needed 17% fewer tokens than when they worked alone,” some tasks that failed solo succeeded, and at scale teams copied and adapted each other’s finished proofs (libcups, freerdp, libzmq). The authors point to Mathlib, where each theorem builds on earlier ones. So the price of a task depends on the state of the proof library as well as the model. Any system that picks a model per task without first retrieving prior proofs is pricing the wrong thing.

The third extension goes back to evaluation. “Encode ‘this test suite always passes’ as the theorem” carries over to any benchmark with an executable oracle. A SWE-bench-style task could come with a proof obligation in place of a pass rate over sampled inputs. Even a small checked subset would give a benchmark that relies on LLM judges something preference votes can’t: ground-truth labels to calibrate the judges against. The spec gap doesn’t go away, and the report itself shows how large it is. Its Python interpreter, written in Rust and proved in Verus, agreed with CPython on 99.95% of 1.7 million random programs. The other 0.05% is where spec and reality disagree, and the checker can’t see that part by construction. Some caveats: this is a lab grading its own models, n=36 is small, and other models’ numbers aren’t reported. Still, the main move holds up. The specs were already sitting in CI, and what changed is the cost of proving them.