Anthropic said it has used its Claude model to automate large portions of formal software verification, collaborating with startup Theorem to generate machine-checked proofs on compiled binaries for 239 fuzzing entry points across 123 open-source libraries. The company claims roughly 180 million lines of proofs—checked by the Rocq kernel and grounded in RISC-V and Linux process semantics—delivered “no-crash” guarantees under defined assumptions and surfaced long-lurking defects missed by extensive fuzzing. The effort converts developer tests into formal specifications, and Anthropic reports growing efficiency as models improve and proofs are reused across projects. Still, the approach depends on trusted machine semantics, focuses on single-threaded static binaries, and does not cover every memory-safety class or deployment environment. Theorem plans to extend the pipeline to additional projects as Anthropic positions LLM-driven verification as a mainstream tool for securing critical software dependencies.
Related articles:
— riscv-formal: A Framework for RISC‑V ISA Formal Verification
— libFuzzer: A Library for Coverage-Guided Fuzz Testing
