AI
Claude writes machine-checked crash proofs for 123 open-source libraries
In work with verification startup Theorem, Anthropic had Claude prove at the RISC-V assembly level that 239 entry points across 123 OSS-Fuzz libraries cannot crash on any input up to 64 MB, producing roughly 180 million lines of Rocq that a proof checker validates rather than a reviewer. Anthropic says the model also found and patched long-standing bugs, and it is publishing a subset of the proofs. The guarantee assumes single-threaded static binaries on Linux with fixed memory.