Aria让代码智能体自由探索，不用手动设计策略，就能把Iris和reglang上所有定理都自动证出来，比之前的方法强太多了。
Aria系统将Claude Code等通用LLM代码智能体与验证框架结合，无需预设策略即自动生成Coq证明。在Iris分离逻辑的4257个引理和Rust标准库的217个引理上，Aria全部证明成功，零失败。在reglang基准上，此前LLM证明器仅能证明八分之一（约40个），Aria则证明了全部318个。在iris-lean的Lean 4移植中，Aria还自动证明了72个未移植引理，表明该方法不限于Coq。所用模型为Claude Opus 4.7。
Harnessing Code Agents for Automatic Software Verification
Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.