生成式人工智能在许多软件工程任务中展现了其价值。尽管仍处于起步阶段，基于大型语言模型（LLM）的证明生成在效率上仍落后于基于LLM的代码生成。本文介绍了AutoVerus，它利用LLM自动生成Rust代码的正确性证明。AutoVerus的设计旨在匹配Verus的独特特性，Verus是一种验证工具，能够使用Rust编写的证明和规范来验证Rust代码的正确性。AutoVerus由一组精心设计和协调的LLM代理组成，这些代理模拟了人类专家在证明构建过程中的三个阶段：初步证明生成、基于通用提示的证明优化以及基于验证错误的证明调试。为了全面评估AutoVerus并促进该领域的未来研究，我们构建了一个包含150个非平凡证明任务的基准套件，这些任务基于现有的代码生成基准和验证基准。我们的评估结果显示，AutoVerus能够自动生成超过90%任务的正确证明，其中超过一半的任务在不到30秒或3次LLM调用内完成。