Technical Summary: KVerus

Problem Statement

Formal verification offers the highest assurance of software correctness but remains difficult to scale to large, evolving systems due to the substantial manual effort required to write proofs, manage dependencies, and adapt to toolchain changes. While Large Language Models (LLMs) have shown promise in automating proof generation, they fail in real-world, multi-module settings. The authors identify the root cause as the Semantic-Structural Gap: LLMs operate on semantic code patterns, whereas formal verification (specifically in Rust using Verus) is governed by rigid structural dependencies, logical entailments, and precise syntax rules.

Current LLM-based approaches suffer from four key limitations:

1. Lack of Contextual Understanding: Inability to reason across modular systems to identify relevant components.
2. Poor Lemma Discovery: Failure to discover and reuse existing lemmas, especially when documentation is incomplete.
3. Fragility to Toolchain Evolution: Inability to adapt when verification toolchains (e.g., Verus) update, causing previously valid proofs to break.
4. Scalability Issues: Reliance on brittle, manually maintained global specifications that cannot evolve with large codebases.

Methodology: KVerus

To bridge the Semantic-Structural Gap, the authors propose KVerus, a retrieval-augmented, self-adaptive verification system. KVerus operates as a pipeline that constructs a dynamic knowledge base and utilizes it to generate and refine proofs. The system consists of four core modules:

1. Preprocessor (Code and Lemma Preprocessing)

• Metadata Dependency Graph: Performs deep static analysis to construct a typed directed graph of the codebase. Nodes represent language objects (functions, types, traits), and edges represent dependencies (type/structure and call/spec).
• Dependent Code Extraction: For a target function, it traverses the graph (up to depth 3) to extract relevant cross-file definitions, signatures, and dependencies, providing a holistic structural view beyond a single file.
• Lemma Extraction: Extracts signatures, preconditions (requires), postconditions (ensures), and locations of all lemma functions.

2. Comprehender (Knowledge Comprehension and Synthesis)

• Semantic Lemma Indexing: Addresses the lack of documentation in real-world projects. It uses an LLM to generate natural language summaries for undocumented lemmas based on their formal specifications. These summaries, along with existing documentation, are vectorized and indexed for Retrieval-Augmented Generation (RAG).
• Auto-updated Verus Knowledge: Periodically parses official Verus documentation to extract up-to-date syntax rules and features (e.g., loop termination clauses). This knowledge base evolves automatically with the toolchain, preventing obsolescence.

3. Prover (Knowledge-Driven Proof Generation)

• Context Assembly: Combines the target function with its extracted dependent code.
• Requirement Analysis: Uses an LLM to analyze the target and dependent code to generate natural language descriptions of the lemmas required for the proof.
• RAG Retrieval: Queries the lemma knowledge base using these descriptions to retrieve relevant lemmas.
• Synthesis: Constructs a structured prompt containing the target, dependencies, and retrieved lemmas to generate an initial proof attempt.

4. Refiner (Error-Driven Proof Refinement)

• Error Triaging: When verification fails, the module classifies errors (e.g., syntax, arithmetic overflow, missing loop invariants) using pattern matching on compiler output.
• Targeted Knowledge Retrieval: Retrieves specific corrective guidance from the Verus knowledge base corresponding to the error type.
• Iterative Refinement: Constructs a new prompt with the error message, the failed code, and the corrective knowledge, asking the LLM to refine the proof. This loop continues until verification succeeds or the maximum iteration limit is reached.

Key Contributions

1. Identification of the Semantic-Structural Gap: The paper formally defines the disconnect between LLM semantic reasoning and the structural rigidity of formal verification as the primary bottleneck for scalability.
2. Self-Adaptive Verification Paradigm: A novel framework that moves beyond static generation to continuous adaptation, allowing the verification system to evolve alongside the codebase and toolchain.
3. Implementation of KVerus: A working system integrating dependency-aware analysis, semantic lemma indexing, and error-driven self-refinement.
4. Real-World Validation: Successful application to the Asterinas Rust OS kernel, specifically the CortenMM memory management module.

Results

The authors evaluated KVerus on three single-file benchmarks (Verus-Bench, MBPP, Human-Eval) and three repository-level benchmarks (MathSpec-Bench, Memory Allocator, CortenMM).

• Single-File Performance: KVerus verified 80.2% of tasks (251/313), outperforming the state-of-the-art AutoVerus (56.9%) and AlphaVerus (24.9%). It also reduced token costs by over 50% compared to AutoVerus.
• Robustness to Toolchain Updates: In experiments across three Verus releases, KVerus demonstrated superior stability. When a breaking change (explicit decreases clauses for loops) was introduced, AutoVerus's success rate dropped by 23.9%, while KVerus's dropped by only 1.2%.
• Repository-Level Performance: On cross-file dependency benchmarks, KVerus achieved a 51.0% success rate, significantly outperforming a multi-round prompting baseline (4.5%).
• Asterinas Case Study: KVerus successfully verified 23 previously unverified functions in the CortenMM module, accounting for 21.0% of the proof code in that module. These proofs were accepted into the kernel mainline and the Verus standard library.
• Ablation Study: Removing Verus knowledge caused the largest drop in single-file performance (highlighting the need for up-to-date syntax rules), while removing code metadata caused the largest drop in repository-level performance (highlighting the need for cross-file context).

Significance and Claims

The paper claims that KVerus represents a significant step toward making formal verification a scalable and sustainable practice for modern, security-critical software. By addressing the Semantic-Structural Gap through a knowledge-centric, self-adaptive architecture, KVerus overcomes the brittleness of previous LLM-based approaches.

The authors emphasize that their work shifts the paradigm from "static, one-shot generation" to "continuous, adaptive verification." They demonstrate that by systematically organizing syntax, semantics, and domain knowledge, it is possible to automate the verification of complex, real-world systems (like an OS kernel) that were previously intractable for automated tools. The successful upstream acceptance of the generated proofs serves as concrete evidence of the system's practical utility and the quality of its output.