Claude reportedly proved no-crash properties for 239 fuzz-test entry points across 123 libraries

3h ago

first seen 3h ago

From fuzz tests to proofs

A fuzz test feeds generated inputs into an entry point to look for crashes. Fuzzing can try enormous numbers of inputs without covering every possibility. Anthropic says it instead turned existing OSS-Fuzz tests into specifications about whether the tests could crash on inputs under 64 MB. The libraries and tests were compiled into RISC-V executables; Claude wrote proofs that the Rocq kernel checked against specifications built using Theorem’s models of RISC-V instructions and Linux processes.

Anthropic says the proof attempts discovered hundreds of bugs. Claude patched code, after which the specification was regenerated and the proof attempted again. In one example the company describes, a copy of a decompressor had an out-of-bounds write triggered only by an input of around 20 MB with a particular layout.

What the result covers

The reported no-crash proofs assume single-threaded, static RISC-V binaries linked against musl libc, a fixed memory budget, and modeled Linux responses and memory layouts. Anthropic says the result covers inputs under 64 MB; it does not establish that the libraries are bug-free. The company notes that AddressSanitizer does not catch every memory-safety bug, that it did not verify every entry point in each library, and that even doing so would not cover an entire library. It also notes that deployed libraries often run on x86 or ARM with glibc.

Theorem has launched OSS Verify, offering free verification to qualifying open-source projects whose maintainers enroll by pull request. Its page describes a proof about a compiled fuzz test for inputs up to 64 MiB, rather than a whole-project crash guarantee. Anthropic says it is publishing a subset of the work, including complete Rocq proofs for fuzz tests that did not require patching, while withholding proofs that might expose an unpatched bug.