Automated formal verification just cleared a bar researchers thought would take years to reach.
A team of researchers built a system called Aria that pairs a general-purpose LLM code agent with a verification harness, then turned it loose on Coq proof libraries — no human expert, no hand-coded proof strategy required. On the reglang benchmark, where previous LLM-based provers solved roughly 12% of theorems, Aria proved all 318. It also proved all 4,257 lemmas across four core modules of Iris, the leading separation logic framework for concurrent and memory-manipulating programs, plus 217 additional lemmas covering Rust's standard libraries. When tested on iris-lean, an unfinished Lean 4 port of Iris, it proved 72 theorems not yet in the port, confirming the approach isn't tied to a single proof language. At the core of the result is an architectural argument: prior systems constrained the model to a fixed human-designed strategy, retrieving premises and predicting tactics one step at a time. Aria instead hands the whole lemma to an Anthropic model identified in the paper, lets it choose its own approach, and enforces soundness through the harness — a proof is accepted only when Coq's own kernel closes it.
Formal verification has long been the gold standard for software correctness, but the expert labor involved has kept it confined to critical infrastructure and academic projects. If a code agent can handle that labor reliably, the economics of verified software change: teams shipping safety-critical systems in aerospace, finance, or systems programming could run proofs as part of a normal CI pipeline rather than hiring specialist consultants.
The 100% coverage figure deserves scrutiny — benchmark scope matters, and Aria was tested on specific curated libraries, not arbitrary production codebases. Still, going from one-in-eight to all-of-them on the same benchmark is not a rounding error.