Ming-Zhi Gao

KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification

KaPilot is presented, a multi-agent framework for automatically generating specifications to verify unsafe Rust memory safety using Kani, and the shuffle-and-implication strategy is applied to systematically determine the best specification from these candidates.