Your Fuzz Harness Is the Spec

Anthropic just proved that 239 OSS-Fuzz entry points don't crash on any input under 64 MB, and every spec was a fuzz test somebody had already written.

Here's what Anthropic and Theorem did. They took 239 entry points across 123 open-source libraries from Google's OSS-Fuzz, turned each existing fuzz test into a statement -- "this never crashes" -- over the compiled RISC-V binary, and had Claude write a proof that the Rocq proof checker accepts. The claim: for every input under 64 MB, the program exits normally, with no memory-safety errors and no failed assertions. Along the way Claude found hundreds of bugs, patched them, and re-proved. All of this is Anthropic's own reporting; nobody outside has replicated it yet.

The proofs are enormous (about 180 million lines of Rocq in total) and no human has to read them -- the checker does. What a human has to read is the spec, and here the spec was a fuzz harness: a few lines of code that take arbitrary bytes and call your library with them.

What Stays Expensive

Whatever an agent does with your code -- fuzz it, refactor it, prove it -- it needs to be told what "correct" means. That part doesn't get automated away.

A fuzz harness is the most boring way to say it. No oracle, no expected output, just "for any input, don't fall over." It's also the one a machine can do the most with: a fuzzer can run it for a week, and as the researchers just showed, a proof can be built on it.

I've long made fixture and snapshot tests a big part of how I test, and I've argued for canary testing in production. Same reason every time: tests that keep paying after you write them. A fuzz harness is the extreme case -- a few lines, and it was enough of a spec to hang a machine-checked proof on.

Write One Today

In Rust, that's cargo-fuzz. cargo install cargo-fuzz, then cargo fuzz init in your crate, and a target like this:

#![no_main]
use libfuzzer_sys::fuzz_target;

fuzz_target!(|data: &[u8]| {
    if let Ok(s) = std::str::from_utf8(data) {
        let _ = my_crate::parse(s);
    }
});

That's the whole spec: for any UTF-8 string, parse returns without panicking. It doesn't care whether the result is Ok or Err, only that you get one. Run it with cargo +nightly fuzz run <target> (it needs nightly for some unstable flags).

In safe Rust this mostly finds panics -- an unwrap on bad input, an out-of-bounds index, overflow in debug builds -- not memory corruption. That's still a crash in production. Then pick the functions that eat untrusted input -- parsers, decoders, anything behind a network port -- and give each one a harness. That's your list of specs.

Where This Stops

Anthropic lists the limits itself, and they matter:

"Formally verified" does not mean "bug-free." If the spec is wrong or too weak, you have a proof of the wrong thing. "Doesn't crash" says nothing about whether parse returns the right numbers.
The machine isn't yours. The proofs assume a static, single-threaded, musl-linked RISC-V binary with a fixed memory budget. Most people ship dynamically linked glibc on x86 or ARM. And none of the verified code here was Rust.
It covers what it covers. Only the verified entry points, memory safety as far as the tooling detects it, no dead code, and nothing about callers misusing the API.
It's expensive. Anthropic says the proofs can take hundreds of millions of tokens.

Don't wait for an agent to prove your service. If this ever becomes routine, the first projects to benefit are the ones that already wrote down what "correct" means, in code -- and most of the time, that means a fuzz harness.