Harnessing Code Agents for Automatic Software Verification
作者: Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel
分类: cs.FL, cs.AI, cs.SE
发布日期: 2026-07-07
💡 一句话要点
提出代码代理以实现自动软件验证
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化验证 大型语言模型 自动证明 软件可靠性 代码代理 验证工具 智能合约 安全性分析
📋 核心要点
- 现有方法依赖固定的证明策略，限制了大型语言模型的灵活性和有效性，导致只能证明部分目标引理。
- 本文提出将整个引理交给通用LLM代码代理，允许其自主选择证明方法，并通过验证工具确保证明的正确性和完整性。
- 实验结果显示，该方法在多个基准上实现了全自动证明，覆盖率达到100%，显著超越了现有的LLM证明器。
📝 摘要（中文）
形式化验证提供了软件正确性的最强保证，但其扩展性不足，交互式定理证明器如Coq需要大量专家努力。大型语言模型（LLMs）有潜力自动生成这些证明，但现有方法通常依赖固定的人为设计的证明策略，限制了模型的灵活性。本文提出将整个引理交给通用LLM代码代理（如Claude Code），并将其包装在验证工具中，从而实现更简单有效的验证，确保每个目标引理都能被证明，无需专家干预。实验表明，该方法在多个基准上均取得了显著的自动化证明能力。
🔬 方法详解
问题定义：本文旨在解决现有形式化验证方法在扩展性和灵活性上的不足，特别是交互式定理证明器如Coq所需的专家干预和固定策略的限制。
核心思路：通过将整个引理交给通用LLM代码代理，允许其自由选择证明策略，结合验证工具的反馈机制，实现全自动的证明过程。
技术框架：整体架构包括一个通用LLM代码代理和一个验证工具，后者提供反馈和约束，确保每个证明的正确性、完整性和终止性。
关键创新：最重要的创新在于不再依赖固定的证明策略，而是允许模型自主探索证明路径，从而实现更高的证明覆盖率和效率。
关键设计：在设计中，验证工具设置了严格的反馈机制，确保每个证明在被接受前必须通过验证器的内核检查，避免未证明的义务或潜在的发散策略。
🖼️ 关键图片
📊 实验亮点
实验结果表明，使用该方法的系统在Iris逻辑上成功证明了4257个引理，并在reglang基准上证明了318个引理，显示出显著的性能提升。与以往的LLM证明器相比，该方法实现了100%的证明覆盖率，且无需专家干预，展现出极高的自动化能力。
🎯 应用场景
该研究的潜在应用领域包括软件开发、编译器验证和安全性分析等。通过实现全自动的形式化验证，能够大幅降低软件开发中的错误率，提高软件的可靠性和安全性，推动智能合约和关键系统的安全验证。未来，该方法有望在更广泛的领域内推广，提升自动化验证的普及性和实用性。
📄 摘要（原文）
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.