KaPilot：用于不安全Rust验证的大语言模型辅助Kani规范生成
KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
AI总结：
研究针对不安全Rust内存安全验证规范编写难题，提出KaPilot多智能体框架，经轻量级分析、智能体协作及循环优化、策略筛选确定最佳规范，评估显示其在规范生成成功率和质量上优于AutoSpec。
AI中文摘要：
Rust的所有权和类型系统提供了强大的内存安全保证，但不安全代码仍存在内存安全风险。形式验证对确保内存安全至关重要，但为不安全的Rust编写精确规范具有挑战性且很大程度上依赖手动。大语言模型在生成形式规范方面有潜力，但往往以代码为中心，易继承实现缺陷且缺乏系统质量评估。本文提出KaPilot，一个多智能体框架，使用Kani自动生成规范以验证不安全Rust的内存安全。过程始于轻量级程序分析和证明框架生成。SafetyReq智能体从目标Rust函数文档中提取简洁精炼的安全要求列表，指导SpecGenerate智能体生成初始规范。然后通过SpecGenerate、SpecPrecheck和SpecVerify智能体参与的生成-预检查-验证循环迭代优化规范。最后应用洗牌和蕴含策略从候选规范中系统确定最佳规范。我们对54个有真实情况和70个无真实情况的不安全Rust函数评估了KaPilot。KaPilot的规范生成成功率分别为88.9%和71.4%，57.4%的生成规范等同于或强于真实情况。与AutoSpec相比，KaPilot产生的可验证规范多14.8%，等同或更好的规范多25.9%。
英文摘要：
Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks. Formal verification is crucial for ensuring memory safety, but writing precise specifications for unsafe Rust is challenging and largely manual. Large language models (LLMs) have shown promise in generating formal specifications but are often code-centric, prone to inheriting implementation flaws, and lack systematic quality assessment. In this paper, we present KaPilot, a multi-agent framework for automatically generating specifications to verify unsafe Rust memory safety using Kani. The process begins with lightweight program analysis and proof harness generation. The SafetyReq agent extracts a concise, refined list of safety requirements from the target Rust function's documentation, which guides the SpecGenerate agent in producing initial specifications that specify memory safety concerns. Then, the specifications are iteratively refined through a generate-precheck-verify loop involving SpecGenerate, SpecPrecheck, and SpecVerify agents, which assess quality and feed errors back. By executing this loop multiple times, KaPilot generates a set of candidate specifications. Finally, the shuffle-and-implication strategy is applied to systematically determine the best specification from these candidates. We evaluated KaPilot on 54 unsafe Rust functions with ground truth and 70 without. KaPilot achieved 88.9% and 71.4% specification generation success, respectively, with 57.4% of generated specifications equivalent to or stronger than the ground truth. Compared with AutoSpec, KaPilot produces 14.8% more verifiable specifications and 25.9% more equivalent-or-better specifications.
