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

Minghua Wang, Yuxi Ling, Mingzhi Gao +2

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 saf…