VeruSAGE: A Study of Agent-Based Verification for Rust Systems

📄 arXiv: 2512.18436v1 📥 PDF

作者: Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R. Lorch, Shan Lu

分类: cs.OS, cs.AI, cs.FL, cs.SE

发布日期: 2025-12-20

💡 一句话要点

VeruSAGE：基于Agent的Rust系统验证研究，提升LLM代码正确性证明能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 系统验证 Rust编程语言 形式化验证 Agent系统 代码正确性 VeruSAGE-Bench

📋 核心要点

  1. 现有方法难以保证LLM生成代码的正确性，尤其是在系统软件这种对可靠性要求极高的领域。
  2. 设计不同的agent系统，针对性地利用不同LLM的优势，弥补其在代码验证方面的不足。
  3. 实验结果表明，特定的LLM-agent组合在系统验证任务上表现出色，验证了LLM辅助系统软件开发的潜力。

📝 摘要（中文）

本文全面研究了大型语言模型（LLMs）在Rust系统软件正确性证明方面的能力。为此，作者构建了一个新的系统验证基准测试集VeruSAGE-Bench，其中包含从八个开源Verus验证的Rust系统中提取的849个证明任务。此外，针对不同LLM（o4-mini、GPT-5、Sonnet 4和Sonnet 4.5）的优势和劣势，设计了不同的agent系统。研究表明，需要不同的工具和agent设置来激发不同类型LLM的系统验证能力。研究中最佳的LLM-agent组合完成了VeruSAGE-Bench中超过80%的系统验证任务，并且完成了超过90%的未包含在VeruSAGE-Bench中的系统证明任务（因为人类专家尚未完成）。这一结果表明，LLM辅助验证系统软件的开发具有巨大的潜力。

🔬 方法详解

问题定义：论文旨在解决大型语言模型（LLMs）在系统软件（特别是用Rust编写的系统软件）的正确性证明方面能力不足的问题。现有的LLM虽然在代码生成方面表现出色，但在严格推理和证明代码正确性方面仍然存在挑战。缺乏一个专门针对系统验证的基准测试集，以及如何有效地利用LLM进行代码验证是当前的痛点。

核心思路：论文的核心思路是设计不同的agent系统，这些agent系统能够针对不同LLM的特点（例如，o4-mini、GPT-5、Sonnet 4和Sonnet 4.5）进行定制，从而最大限度地发挥它们在系统验证方面的能力。通过将LLM与合适的工具和策略相结合，可以弥补LLM在推理和证明方面的不足。

技术框架：整体框架包括以下几个主要步骤：1) 构建VeruSAGE-Bench基准测试集，该数据集包含从Verus验证的Rust系统中提取的证明任务。2) 针对不同的LLM，设计不同的agent系统，这些agent系统可能包括代码生成、测试用例生成、形式化验证等模块。3) 使用不同的LLM-agent组合在VeruSAGE-Bench上进行实验，评估其在系统验证任务上的表现。4) 分析实验结果，找出最佳的LLM-agent组合，并探讨不同组合的优缺点。

关键创新：该论文的关键创新在于提出了一个基于agent的系统验证方法，该方法能够根据不同LLM的特点进行定制，从而提高LLM在系统验证任务上的表现。此外，VeruSAGE-Bench基准测试集的构建也为系统验证领域的研究提供了有价值的资源。

关键设计：论文的关键设计包括：1) VeruSAGE-Bench基准测试集的构建，需要仔细选择和提取具有代表性的证明任务。2) agent系统的设计，需要考虑如何将LLM与合适的工具和策略相结合，例如，可以使用形式化验证工具来验证LLM生成的代码，或者使用测试用例生成器来评估代码的正确性。3) 实验评估的设计，需要选择合适的评估指标，例如，完成的证明任务数量、证明的正确性等。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，最佳的LLM-agent组合在VeruSAGE-Bench基准测试集上完成了超过80%的系统验证任务。更重要的是，该组合还完成了超过90%的未包含在VeruSAGE-Bench中的系统证明任务，这些任务之前尚未被人类专家完成。这表明LLM在系统验证方面具有超越人类专家的潜力。

🎯 应用场景

该研究成果可应用于自动化软件验证、形式化方法、以及LLM辅助的软件开发流程中。通过利用LLM的能力，可以降低系统软件验证的成本，提高软件的可靠性和安全性。未来，该方法可以扩展到其他编程语言和系统软件领域，促进可信软件的开发。

📄 摘要（原文）

Large language models (LLMs) have shown impressive capability to understand and develop code. However, their capability to rigorously reason about and prove code correctness remains in question. This paper offers a comprehensive study of LLMs' capability to develop correctness proofs for system software written in Rust. We curate a new system-verification benchmark suite, VeruSAGE-Bench, which consists of 849 proof tasks extracted from eight open-source Verus-verified Rust systems. Furthermore, we design different agent systems to match the strengths and weaknesses of different LLMs (o4-mini, GPT-5, Sonnet 4, and Sonnet 4.5). Our study shows that different tools and agent settings are needed to stimulate the system-verification capability of different types of LLMs. The best LLM-agent combination in our study completes over 80% of system-verification tasks in VeruSAGE-Bench. It also completes over 90% of a set of system proof tasks not part of VeruSAGE-Bench because they had not yet been finished by human experts. This result shows the great potential for LLM-assisted development of verified system software.