Formal verification provides the highest assurance of software correctness and security, but its application to large-scale, evolving systems remains a major challenge. While large language models (LLMs) have shown promise in automating proof generation, they often fail in real-world settings due to their inability to handle complex cross-module dependencies or changes in the codebase or the verification toolchain. We identify the fundamental problem as the Semantic-Structural Gap: LLMs operate on semantic code patterns, whereas formal verification is governed by rigid structural dependencies, a disconnect that leads to brittle, unsustainable proofs. To bridge this gap, we propose a new paradigm of self-adaptive verification and present KVerus, a retrieval-augmented system for Verus-based Rust verification that can adapt to an evolving software environment. KVerus constructs a dynamic knowledge base of code metadata, lemma semantics, and toolchain specifics. By combining dependency-aware program analysis, semantic lemma indexing, and error-driven self-refinement, it can navigate intricate cross-file dependencies to synthesize proofs and automatically repair proofs when faced with common evolutionary changes. Across three single-file benchmarks, KVerus verifies 80.2% of tasks, outperforming the state-of-the-art AutoVerus (56.9%) and degrades less than AutoVerus under breaking Verus updates. On three repository-level benchmarks with cross-file dependencies, KVerus achieves a 51.0% success rate, compared to 4.5% for a multi-round prompting baseline. Finally, on the Asterinas Rust OS kernel, KVerus produces upstream-accepted proofs that verify 23 previously unverified functions (21.0% of proof code) in the memory-management module. KVerus represents a significant step towards making formal verification a scalable and sustainable practice for modern, security-critical software.

翻译：形式化验证能为软件的正确性与安全性提供最高级别的保证，但将其应用于大规模且持续演化的系统仍是重大挑战。尽管大语言模型在自动化证明生成方面展现出潜力，但在实际场景中仍常因无法处理复杂的跨模块依赖、代码库或验证工具链的变更而失败。我们将根本问题识别为"语义-结构鸿沟"：大语言模型基于语义代码模式运作，而形式化验证遵循严格的结构化依赖关系，这种脱节导致证明的脆弱性与不可持续性。为弥合这一鸿沟，我们提出自适应验证的新范式，并实现KVerus系统——一种基于检索增强的Verus Rust验证框架，能适应不断演化的软件环境。KVerus构建包含代码元数据、引理语义及工具链细节的动态知识库。通过结合依赖感知的程序分析、语义引理索引与错误驱动的自我优化，该系统能够导航复杂的跨文件依赖关系以合成证明，并在面对常见演化变更时自动修复证明。在三个单文件基准测试中，KVerus验证了80.2%的任务，显著优于现有最优系统AutoVerus（56.9%），且在遭遇破坏性Verus更新时性能下降更少。在三个包含跨文件依赖的仓库级基准测试中，KVerus实现了51.0%的成功率，而多轮提示基线方法仅为4.5%。最后，在Asterinas Rust操作系统内核中，KVerus生成了已被上游采纳的证明，验证了内存管理模块中23个先前未验证的函数（占证明代码的21.0%）。KVerus标志着向实现安全关键型现代软件中可扩展、可持续的形式化验证实践迈出的重要一步。