Anthropic and Theorem Labs released a report showing that Claude generated about 180 million lines of Rocq proof code for 239 program entry points across 123 open-source libraries, discovering and fixing hundreds of bugs, and for the first time applied formal verification to production software at the assembly instruction level (RISC-V) at scale.