Appendix: LLMs are making formal software verification feasible at a much larger scale

Oct 22, 2026 research: Claude + Theorem proved no-crash properties for 239 OSS-Fuzz entry points across 123 libraries on RISC-V ASan binaries; ~180M lines of checked Rocq proof. Scope: single-threaded static RISC-V/musl, inputs under 64 MiB, modeled Linux semantics.