tl;dr: Anthropic and Theorem used Claude to generate formal correctness proofs for 123 open-source libraries at the RISC-V assembly level, producing ~180 million lines of Rocq proofs that show the compiled binaries won't crash on any input under 64MB (given certain assumptions). The process also uncovered longstanding bugs that fuzzers had missed, including one requiring 20MB inputs with specific layouts. The authors argue that LLMs are making formal verification—traditionally requiring years of expert effort—newly practical at scale, with proof reuse and improving model efficiency driving costs down further.