A Hundred and Eighty Million Lines of Proof
Anthropic and Theorem published a large-scale formal verification effort where Claude wrote ~180 million lines of Rocq proofs, proving no-crash properties for 239 OSS-Fuzz entry points at compiled RISC-V binary level. The work found hundreds of bugs—including ones fuzzing had missed for years—and forces an honest look at what "formally verified" can and can't mean.
Read more →