Anthropic and Theorem report Claude-generated, machine-checked proofs in Rocq for 239 OSS-Fuzz entry points across 123 libraries. The target differs from earlier helper-lemma work: these proofs model RISC-V execution and Linux semantics for static binaries built with musl, under a deliberately bounded environment—single-threaded execution, fixed memory and inputs below 64 MB.
The artifacts are enormous. The effort produced about 180 million lines of proof; for a typical target, roughly 600,000 proof lines accompanied 18,000 RISC-V instructions, or about 33 proof lines per instruction. The work also found hundreds of bugs, including large-input failures, multi-handle interactions and logic errors.
On a 36-task benchmark, Anthropic says Opus 5.5 used about 40% fewer tokens than Opus 5, while a shared proof workspace reduced token use by 17%. Rocq and the modeled hardware, OS and compiler semantics remain in the trusted base, and a verified implementation does not stop callers from misusing an API.