一句话：提出 AutoVerus，用 LLM 智能体网络自动为 Rust 代码生成 Verus 正确性证明，90%+ 任务成功。
本文关注 LLM 驱动的形式化证明生成明显落后于代码生成的问题，提出 AutoVerus，一个面向 Rust 代码的自动正确性证明生成方法。AutoVerus 适配 Verus 验证工具的特性：规范与证明同样用 Rust 编写。其核心是由多个 agent 组成的网络，模仿人类专家证明构建的三阶段流程：初步证明生成、基于通用提示的证明精化，以及基于验证错误的证明调试。为系统评估，作者基于已有代码生成与验证基准构建了包含 150 个非平凡证明任务的基准套件。实验表明，AutoVerus 能为超过 90% 的任务自动生成正确证明，且超过一半任务在 30 秒或 3 次 LLM 调用内完成。
Generative AI has shown its value for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present A uto V erus . A uto V erus uses LLMs to automatically generate correctness proof for Rust code. A uto V erus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. A uto V erus consists of a network of agents that are crafted and orchestrated to mimic human experts’ three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate A uto V erus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that A uto V erus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.
@article{paperbot2883,
title = {AutoVerus: Automated Proof Generation for Rust Code},
author = {Chenyuan Yang and Xuheng Li and Md Rakib Hossain Misu and Jianan Yao and Weidong Cui and Yeyun Gong and Chris Hawblitzel and Shuvendu Lahiri and Jacob R. Lorch and Shuai Lu and Fan Yang and Ziqiao Zhou and Shan Lu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763174}
}