[Paper] 可调自动化在自动化程序验证中

Source: arXiv - 2512.03926v1

Overview

本文提出了一种用于基于 SMT 的程序验证器的 可调自动化 机制。通过让开发者控制在验证过程中可用的量化事实，作者实现了在“只需点击”式的高度自动化便利性与更精简、手动证明风格的速度之间的平衡。该技术已在面向 Rust 的验证器 Verus 中实现，并在真实的开源项目上进行评估，展示了选择性量化管理如何在不牺牲正确性的前提下显著影响验证时间。

Key Contributions

• 细粒度量化控制：一种语言层面的构造，允许库作者暴露多个预定义的自动化层级（例如 “fast”、 “balanced”、 “full”）。
• 用户驱动的自定义：终端用户可以在模块、函数甚至证明上下文粒度上覆盖默认层级。
• 与 Verus 的集成：该机制内置于 Verus 的类 Rust 语法中，保持了系统程序员使用该工具的便利性。
• 实证评估：在多个公开可用的 Rust 代码库上进行基准测试，展示了在自动化光谱上验证时间与证明工作量之间的可衡量权衡。
• 设计指南：作者提供了实用的建议，帮助库作者在不让用户不堪重负的前提下，暴露有用的自动化层级。

Methodology

1. 量化可用性模型 – 作者将每个量化公理（例如关于数据结构的引理）视为一种 资源，可以在特定验证上下文中开启或关闭。
2. 自动化层级 – 库代码可以在命名层级下声明一组公理（例如 #[automation = "fast"]）。验证引擎随后仅加载属于所选层级的公理。
3. 上下文覆盖 – 通过轻量注解 (#[use_level = "full"])，开发者可以在局部为特定函数或证明块请求更多（或更少）的公理。
4. 在 Verus 中的实现 – 团队扩展了 Verus 前端以解析这些注解，并修改底层 SMT 驱动，在每次证明查询前动态调整实例化的量化集合。
5. 评估设置 – 他们选取了三个 Rust 项目（一个密码学库、一个并发数据结构库和一个系统级驱动），在每个自动化层级下运行 Verus，测量总验证时间、超时次数以及所需的手动证明提示数量。

Results & Findings

• 性能与工作量的权衡： “fast” 设置可将验证时间缩短最多 20 %，但会迫使开发者添加更多显式的证明提示。 “full” 设置则能消除大量超时，却会导致明显的运行时下降。
• 选择性覆盖的收益：仅对少数热点函数使用 “full” 层级，就能恢复大部分鲁棒性优势，同时保持整体运行时间接近 “balanced” 基准。
• 开发者体验：库作者报告称，暴露自动化层级后，下游用户因验证超时而提交的支持工单数量显著减少。

Practical Implications

• 库设计：在发布已验证的 Rust crate 时，可以随包提供多个自动化配置文件，让下游项目根据 CI 流水线的需求选择合适的平衡点。
• CI/CD 集成：团队可以在每个 Pull Request 上运行快速验证，在夜间构建时切换到更彻底的层级，从而在不拖慢日常开发的前提下捕获细微错误。
• 性能关键领域：在安全关键或高保证系统（如嵌入式固件、密码学原语）中，仅在需要的地方提升自动化程度，可使验证预算保持在可接受范围。
• 工具生态：该概念具备可移植性——其他基于 SMT 的验证器（如 Dafny、Why3）也可以采用类似的量化可用性 API，推动跨语言的自动化调优方法更加统一。

Limitations & Future Work

• 量化粒度：当前模型在整个公理层面工作；更细粒度的控制（例如每个实例化模式）仍未探索。
• 用户易用性：虽然注解轻量，但开发者仍需了解每个层级的性能影响，这可能需要工具支持（如可视化仪表盘）。
• 对超大代码库的可扩展性：评估覆盖的是中等规模项目；作者指出，极大的单体仓库可能表现出不同的扩展特性。
• 跨工具验证：未来工作包括在其他验证框架中原型化该方法，并研究其与替代量化实例化策略（如 E‑matching、基于模型的量化实例化）的交互。

Bottom line: 可调自动化为验证工程师提供了一个实用的旋钮，以在速度和证明力度之间取得平衡，将“全有或全无”的量化困境转化为灵活、友好的开发工作流。

Authors

• Alexander Y. Bai
• Chris Hawblitzel
• Andrea Lattuada

Paper Information

• arXiv ID: 2512.03926v1
• Categories: cs.SE, cs.LO, cs.PL
• Published: December 3, 2025
• PDF: Download PDF