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 采用一个规划器模块来协调抽象、类型不变量、规范和证明代码的系统性生成。为了解决大型语言模型（LLMs）经常误解 Verus 的注释语法和验证特定语义的挑战，VeriStruct 在提示中嵌入了语法指导，并包含一个修复阶段来自动纠正注释错误。在对十一个 Rust 数据结构模块的评估中，VeriStruct 在十一个模块中成功验证了十个，总共成功验证了 129 个函数中的 128 个（99.2%）。这些结果代表了向实现 AI 辅助的自动化形式验证目标迈出的重要一步。
相关内容
微信扫码咨询专知VIP会员