一句话：提出 LLM 辅助的 Verus 证明生成工作流 KVerus，用动态知识库支持仓库级跨文件证明生成与修复。
仓库级形式化验证在 Rust 系统中逐渐可行，但在真实项目里维护和扩展证明仍然代价高昂。以 Asterinas 的 CortenMM 内存管理模块为例，Verus 证明需要跨文件和模块边界、复用文档稀少的项目专有引理，并适应 Verus/工具链的频繁演进。现有基于 LLM 的证明生成方法多面向小规模或单文件任务，缺乏项目结构知识与验证器感知的修复能力。KVerus 构建覆盖代码元数据、引理语义与 Verus/工具链知识的动态知识库，结合依赖感知上下文提取、语义引理检索和错误驱动精化来生成 Verus 证明代码，并由验证器检查、工程师复核。在 CortenMM 中，生成的补丁验证了 23 个此前未被验证的函数，引入 6 个可复用引理，占该模块证明代码的 21.0%，并被 Asterinas 上游接受。在跨文件依赖的仓库级基准上成功率为 51.0%，而多轮提示基线仅为 4.5%；在单文件基准上验证了 80.2% 的任务。
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. This paper presents KVerus, a practical LLM-assisted workflow for Verus proof generation in evolving Rust repositories. KVerus builds a dynamic knowledge base over code metadata, lemma semantics, and Verus/toolchain knowledge. It combines dependency-aware context extraction, semantic lemma retrieval, and error-driven refinement to generate Verus proof code that is checked by the verifier and then reviewed by engineers. In CortenMM, KVerus generated verifier-passing proof patches that verified 23 previously unverified functions, introduced 6 reusable lemmas, and accounted for 21.0% of the proof code in the module; these patches were accepted upstream by Asterinas developers. The CortenMM experience also exposed practical boundary cases, including incorrect specifications that required human repair and generated proofs that benefited from human cleanup. Across benchmarks, KVerus achieves a 51.0% success rate on three repository-level benchmarks with cross-file dependencies, compared with 4.5% for a multi-round prompting baseline, and verifies 80.2% of tasks on three single-file benchmarks. These experiences and results show that LLM-assisted proof generation can move beyond benchmark-oriented synthesis and become a maintainable workflow for repository-scale Rust verification.
@inproceedings{abs-2605-03822,
title = {KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code},
author = {Yuwei Liu and Xinyi Wan and Yanhao Wang and Minghua Wang and Lin Huang and Tao Wei},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3834503}
}