VeriStruct：面向Verus数据结构模块的AI辅助自动化验证
软件工程
2026-03-04 v4 人工智能
摘要
我们提出VeriStruct，这是一个新型框架，将AI辅助自动化验证从单个函数扩展到Verus中的更复杂的数据结构模块。VeriStruct采用规划器模块来协调系统性地生成抽象、类型不变性、规范和证明代码。为解决LLM常常误解Verus注释语法和验证特定语义的挑战，VeriStruct在提示中嵌入语法指导，并包含一个修复阶段用于自动纠正注释错误。在对十一个Rust数据结构模块进行的评估中，VeriStruct在十个模块中成功，其中总共验证了128个129个函数（99.2%）。这些结果标志着自动AI辅助形式化验证目标取得的重要进展。
引用
@article{arxiv.2510.25015,
title = {VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus},
author = {Chuyue Sun and Yican Sun and Daneshvar Amrollahi and Ethan Zhang and Shuvendu Lahiri and Shan Lu and David Dill and Clark Barrett},
journal= {arXiv preprint arXiv:2510.25015},
year = {2026}
}