KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code

摘要

Repository-scale formal verification is becoming practical for Rust systems, but maintaining and extending proofs remains expensive in real projects. In the Asterinas Rust OS kernel, the CortenMM memory-management module requires Verus proofs that cross file and module boundaries, reuse project-specific lemmas with limited documentation, and survive frequent Verus/toolchain evolution. Existing LLM-based proof-generation methods are mostly designed for small or single-file tasks, and they do not provide the structural project knowledge or verifier-aware repair needed in such a repository-scale verification workflow.