VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

本文介绍了 VeriStruct，这是一个将 AI 辅助自动化验证从单一函数扩展至复杂数据结构模块的新框架，它通过规划器协调抽象与规范生成，并利用语法引导和自动修复机制解决 Verus 注解理解难题，在 11 个 Rust 模块的评估中成功验证了 99.2% 的函数。

要点

这篇文章介绍了一个名为 VeriStruct 的新工具，它的核心任务是利用人工智能（AI）来自动检查计算机代码中的“数据结构”是否安全、无漏洞。

为了让你更容易理解，我们可以把这篇论文的内容想象成**“给一座复杂的乐高城堡请了一位 AI 建筑监理”**。

1. 背景：为什么我们需要这个？

想象一下，现在的程序员（或者 AI 助手）正在用乐高积木搭建各种复杂的城堡（也就是软件中的“数据结构”，比如队列、树、地图等）。

• 问题：虽然 AI 能很快搭出城堡，但它可能会偷偷把承重墙搭歪，或者把地基打得不稳。一旦城堡建好了再发现这些问题，拆掉重来的代价太大了。
• 传统方法：以前，我们需要请一位极其专业的“人类建筑监理”（形式化验证专家），他需要逐行检查每一块积木的摆放是否符合物理定律（数学逻辑），并写下厚厚的检查报告（代码注释/规范）。但这非常耗时、昂贵，而且只有少数专家能懂。
• 新挑战：现在的 AI 虽然聪明，但它不懂“建筑监理”的专用术语（Verus 的语法），经常乱写检查报告，导致真正的监理（验证器）看不懂，直接报错。

2. VeriStruct 是什么？

VeriStruct 就是一个**"AI 建筑监理团队”。它不只是让 AI 随便写写，而是设计了一套系统化的工作流程**，专门用来给复杂的乐高城堡（数据结构模块）做自动检查。

它的工作流程就像是一个**“规划师 + 施工队 + 质检员”**的闭环：

第一步：规划师（Planner）

在开始干活前，VeriStruct 先派出一位**“规划师”**。

• 作用：它先看看这座城堡长什么样，决定需要哪些检查步骤。
• 比喻：就像盖房子前，规划师会判断：“这座房子需要画结构图（View），需要定承重规则（类型不变量），还需要写操作手册（规范），最后还要现场演练（证明代码）。”
• 聪明之处：如果某个小房子不需要复杂的承重规则，规划师就会跳过那一步，避免浪费 AI 的精力。

第二步：施工队（生成模块）

根据规划师的指令，AI 开始生成具体的“检查报告”：

1. 抽象图（View）：把复杂的乐高积木（比如圆环缓冲区）简化成一张简单的逻辑图纸。
   • 比喻：原本圆环缓冲区内部有很多复杂的指针和索引，AI 把它抽象成“一个排队的人流”，这样监理更容易看懂。
2. 承重规则（Type Invariant）：规定积木必须满足的条件（比如“头指针永远不能大于尾指针”）。
3. 操作手册（Specifications）：规定每个动作（如“放入积木”、“取出积木”）前后的状态变化。
4. 现场演练（Proof Blocks）：给验证器提供具体的线索，帮助它通过数学证明。

第三步：质检员与修理工（Repair Stage）

这是 VeriStruct 最厉害的地方。

• 问题：AI 生成的报告经常有错。比如，它可能用错了术语，或者逻辑不通。真正的“监理”（Verus 验证器）会报错说：“这里不行，因为你在检查报告里用了‘施工动作’而不是‘逻辑描述’。”
• 解决：VeriStruct 有一个**“修理工”**。
  • 当验证器报错时，修理工会分析错误信息（比如“你混淆了执行函数和逻辑函数”）。
  • 然后，修理工会自动重写那部分 AI 生成的代码，修正错误，再重新提交验证。
  • 这个过程会循环多次，直到所有错误都被修好，或者达到最大尝试次数。

3. 它做得怎么样？（实验结果）

作者找了 11 个 不同的复杂乐高城堡（11 种 Rust 数据结构，如环形缓冲区、树、位图等）进行测试。

• 成果：VeriStruct 成功帮 10 个 城堡通过了所有检查，总共验证了 129 个功能中的 128 个（成功率高达 99.2%）。
• 对比：
  • 如果只用普通的 AI（没有规划师和修理工），只能搞定 4 个城堡，验证 52 个功能。
  • 即使是目前很厉害的 AI 编程助手（Claude Code），也只能搞定 8 个城堡，验证 102 个功能。
• 结论：VeriStruct 的“规划 + 生成 + 修复”这套组合拳，比单纯让 AI 瞎猜要有效得多。

4. 核心创新点总结（用大白话讲）

1. 从“单点”到“整体”：以前的 AI 验证只能检查单个函数（比如“这个加法对不对”），VeriStruct 能检查整个数据结构模块（比如“这个队列在并发操作下会不会乱套”）。
2. 懂行话：它把 Verus 的专用语法（那些让 AI 头疼的规则）写进了提示词（Prompt）里，教 AI 怎么说话。
3. 自我纠错：它不指望 AI 一次做对，而是设计了专门的“修理工”模块，像人类调试代码一样，根据报错信息自动修补，直到完美。

5. 未来的展望

作者说，现在还需要人工提供“测试用例”（比如告诉 AI 这座城堡要承受什么样的压力测试）。未来他们希望 AI 能自己生成这些测试用例，甚至用“强化学习”让 AI 在不断的试错中变得更聪明，最终实现全自动的、零人工干预的代码安全验证。

一句话总结：
VeriStruct 就像是一个懂行、会规划、还能自动修 bug 的 AI 建筑监理，它让原本只有专家才能做的复杂代码安全验证，变得自动化且高效，极大地降低了软件出错的概率。

技术摘要

VeriStruct 技术总结：基于 AI 辅助的 Verus 数据结构模块自动化验证

1. 研究背景与问题定义

背景

随着生成式 AI 在代码生成中的广泛应用，软件生产力的提升伴随着代码正确性和安全性的风险增加。程序验证（Program Verification）通过数学证明代码无缺陷，是缓解这一风险的关键手段。然而，传统形式化验证（如使用 Verus 工具）需要开发者手动编写复杂的逻辑注解（如前置条件、后置条件、不变式等），这一过程耗时且需要极高的专业知识，限制了其在实际中的大规模应用。

核心挑战

现有的 AI 辅助验证研究主要集中在单一函数的验证上，而本文旨在解决数据结构模块（Data-Structure Modules）的验证问题，这面临两大主要挑战：

1. 验证复杂性：数据结构验证比单一函数更复杂，通常需要：
   • 数学抽象（Mathematical Abstraction）：将具体实现映射为逻辑对象（如序列、集合）。
   • 类型不变式（Type Invariants）：定义数据结构实例必须满足的持久属性。
   • 多方法联合验证：多个方法需在共享的类型不变式下进行联合验证。
2. LLM 对 Verus 语法的理解局限：大型语言模型（LLM）缺乏对 Verus 专用语法（如 spec 函数、view 特性）和验证特定语义（如纯函数限制、所有权系统）的深刻理解，容易产生语法错误或逻辑谬误（例如在注解中调用可执行函数）。

2. 方法论：VeriStruct 框架

VeriStruct 是一个基于 Verus（Rust 的形式化验证扩展）的 AI 辅助自动化验证框架。它采用规划器（Planner）驱动的两阶段流水线，通过系统化的生成与修复机制，将原始 Rust 代码转化为通过验证的注解代码。

2.1 输入与输出

• 输入：待验证的 Rust 源代码（无注解）+ 单元测试套件（用于定义预期行为和排除平凡解）。
• 输出：包含完整 Verus 注解的验证通过代码。

2.2 核心工作流

阶段一：注解生成（Generation Stage）

该阶段由一个规划器（Planner）协调，决定需要生成哪些类型的注解，并依次调用专用模块。

1. 规划器（Planner）：分析代码，决定执行哪些模块。

   • View 模块：生成数学抽象（View Trait），将数据结构映射为逻辑类型（如 Seq, Set）。
   • 类型不变式模块（Type Invariant）：生成字段间的约束关系（如索引范围、容量检查）。
   • 规范模块（Specifications）：生成前置/后置条件（requires/ensures）及规范函数。
   • 证明块模块（Proof Blocks）：生成证明提示（proof blocks）和循环不变式。
   • 策略：并非所有模块都需要执行，规划器根据数据结构特性（如是否存在非平凡字段关系）动态选择。

2. 提示工程（Prompt Engineering）：

   • 每个模块的 Prompt 包含：任务目标、Verus 语法指南（从官方文档提取）、分步指令、少样本学习示例（In-context learning）以及待验证代码和测试。
   • View 细化：针对 LLM 倾向于生成“笛卡尔积”式（过于具体）的 View 的问题，引入了细化步骤，引导 LLM 生成更抽象、更简洁的逻辑视图。

3. 采样策略：每个模块调用时生成 $n$ 个样本，选择验证通过率最高的结果。

阶段二：注解修复（Repair Stage）

由于 LLM 生成的初始注解常包含错误，系统进入迭代修复循环：

1. 错误检测：运行 Verus 验证器，捕获最高优先级的错误信息。
2. 错误分类与路由：通过正则匹配将错误分类，路由到特定的修复模块。
   • 修复模块包括：模式误用（如调用可执行函数）、可变性系统不一致、前后条件冲突、算术溢出、逻辑类型不匹配、测试断言失败等。
   • 测试断言修复：特别设计了模块进行过程间分析，识别导致断言失败的方法，并强化其后置条件。
3. 迭代执行：重复“验证 - 修复”过程，直到所有错误消除或达到最大迭代次数（$m$）。

3. 关键贡献

1. 新的 LLM 辅助工作流：首次将 AI 辅助验证从单一函数扩展到复杂的数据结构模块，引入了数学抽象和类型不变式的协同生成机制。
2. VeriStruct 工具实现：构建了一个包含规划器、多专用生成模块和针对性修复模块的完整系统。
3. 语法与语义引导：通过嵌入结构化的语法指南和专门的修复模块，有效解决了 LLM 对 Verus 特定语义理解不足的问题。
4. 实证评估：在 11 个 Rust 数据结构基准测试上进行了全面评估，证明了该方法的有效性。

4. 实验结果

• 数据集：11 个 Rust 数据结构模块（包括环形缓冲区、位图、树映射、读写锁等），共 129 个待验证函数。
• 主要指标：
  • 成功率：VeriStruct 成功验证了 10/11 个模块。
  • 函数覆盖率：成功验证了 128/129 个函数，准确率达到 99.2%。
  • 对比基线：
    • 相比简单的“生成 - 重试”基线（Baseline），VeriStruct 验证的函数数量提升了 146.2%（从 52 个提升至 128 个）。
    • 相比具备自主工具调用能力的 Claude Code（使用 Claude Sonnet 4.5），VeriStruct 在验证函数数量（128 vs 102）和基准测试解决数量（10 vs 8）上均表现更优，且 Token 消耗更低（22k vs 24k）。
• 案例分析：在位图（Bitmap）基准测试中，LLM 甚至生成了与人类专家不同的、但更简洁有效的抽象方案（将位图抽象为单一数组而非二维数组），展示了 AI 的创造性。

5. 意义与未来展望

意义

• 降低验证门槛：大幅减少了开发者手动编写形式化注解的工作量，使得形式化验证在 Rust 生态中的规模化应用成为可能。
• 提升代码质量：通过自动验证 AI 生成或人类编写的代码，显著降低了引入安全漏洞和逻辑错误的风险。
• 方法论创新：证明了“规划 + 生成 + 修复”的闭环工作流在处理复杂形式化任务时优于单纯的端到端生成。

未来工作

• 检索增强生成（RAG）：集成 Verus 标准库的引理检索，辅助证明合成。
• 并发验证：支持 Verus 资源代数库的生成，以验证更复杂的并发数据结构。
• 自动测试生成：利用 LLM 自动生成高覆盖率的单元测试，进一步减少人工输入。
• 强化学习（RL）：利用验证器的反馈信号训练模型，优化注解策略的探索空间。

综上所述，VeriStruct 代表了 AI 辅助形式化验证领域的重要进展，成功将验证能力从简单的算法扩展到了实际工程中的核心数据结构模块。