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

The proofs cover 239 entry points across 123 open-source libraries, and over the span of a few weeks the work was completed. The proof system is Rocq (formerly Coq), checked by the Rocq kernel, at RISC-V assembly level, with a model of running binaries on Linux. The output is about 180 million lines of Rocq, and a typical proof is about 600,000 lines. Theorem, a formal-methods company, worked on the project with Anthropic. Bugs surfaced during the proof work, hundreds of them, plus an unexploitable corner case in about six zlib-style libraries. The post also names the main bottleneck: the proofs can take hundreds of millions of tokens to produce. An earlier Anthropic project followed a similar pattern. Claude formalized Fermat's Last Theorem in Lean, working largely autonomously over 11 days, though that effort verifies a known proof in a proof assistant; it does not establish a new mathematical result. For a team building an AI product, cost is the main question. Token spend per proof limits how much of a codebase can be verified, so scoping proofs to security-critical entry points is the likely starting point. Anthropic expects formal verification to become an essential part of secure software development as models improve, so founders selling code generation or security tooling may soon face buyers who ask for proofs, not just test coverage.