论文
KaPilot：LLM 辅助生成 unsafe Rust 内存安全验证的 Kani 规约
KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
摘要
Rust 的所有权与类型系统提供了较强的内存安全保证，但 unsafe 代码仍存在内存安全风险。形式化验证十分重要，而为 unsafe Rust 编写准确规约仍具挑战且主要依赖手工。大语言模型能够辅助生成形式化规约，但现有方法常以代码为中心，容易继承实现缺陷，也缺乏系统性质量评估。论文提出多 Agent 框架 KaPilot，自动生成用于 Kani 内存安全验证的规约。流程从轻量程序分析与证明测试框架生成开始；SafetyReq Agent 从目标函数文档提取简明的安全要求，指导 SpecGenerate 生成初始规约。随后，SpecGenerate、SpecPrecheck 和 SpecVerify 在生成—预检查—验证循环中评估质量、反馈错误并迭代修订。重复执行后得到多份候选规约，再通过 shuffle-and-implication 策略系统选择最佳规约。研究在有参考规约的 54 个 unsafe Rust 函数和无参考规约的 70 个函数上评估，规约生成成功率分别为 88.9% 和 71.4%，其中 57.4% 的生成规约与参考规约等价或更强。相较 AutoSpec，可验证规约增加 14.8%，等价或更强规约增加 25.9%。