We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs a planner module to orchestrate the systematic generation of abstractions, type invariants, specifications, and proof code. To address the challenge that LLMs often misunderstand Verus' annotation syntax and verification-specific semantics, VeriStruct embeds syntax guidance within prompts and includes a repair stage to automatically correct annotation errors. In an evaluation on eleven Rust data structure modules, VeriStruct succeeds on ten of the eleven, successfully verifying 128 out of 129 functions (99.2%) in total. These results represent an important step toward the goal of automatic AI-assisted formal verification.

翻译：本文介绍VeriStruct，这是一种新颖的框架，它将AI辅助的自动化验证从单一函数扩展到Verus中更复杂的数据结构模块。VeriStruct采用规划器模块来协调抽象、类型不变量、规范及证明代码的系统性生成。针对大型语言模型常误解Verus注解语法与验证特定语义的挑战，VeriStruct在提示中嵌入语法引导，并包含修复阶段以自动修正注解错误。在对十一个Rust数据结构模块的评估中，VeriStruct在十一个模块中成功验证了十个，总计成功验证了129个函数中的128个（99.2%）。这些成果标志着向AI辅助自动化形式验证目标迈出了重要一步。