TLDR: This paper introduces RVBench, the first benchmark for repository-level program verification in Verus, and RagVerus, a retrieval-augmented generation framework. RagVerus uses context-aware prompting and retrieval strategies (few-shot examples and dependency retrieval) to help large language models synthesize proofs for multi-module software. It significantly improves proof pass rates on existing benchmarks and achieves a 27% relative improvement on the new, more challenging RVBench, demonstrating a scalable approach to automating formal verification for complex, real-world software projects.
In the world of software development, ensuring that programs work exactly as intended, without any errors or vulnerabilities, is a monumental task. For critical systems like operating systems or financial infrastructure, even a tiny flaw can have catastrophic consequences. This is where formal verification comes in – a rigorous process that uses mathematical proofs to guarantee a program’s correctness, going far beyond what traditional testing can achieve.
While formal verification offers exhaustive guarantees, it’s notoriously labor-intensive, demanding deep expertise to construct complex proofs. This challenge becomes even more pronounced in large, real-world software projects where code spans multiple interdependent modules, making proof construction and premise selection incredibly difficult.
Recent advancements in large language models (LLMs) have shown immense promise in automating parts of this process, particularly in generating code and proofs. However, most existing LLM-based methods have focused on isolated, function-level verification tasks, largely overlooking the significant hurdles of verifying entire software repositories.
A new research paper, “Towards Repository-Level Program Verification with Large Language Models,” by Si Cheng Zhong and Xujie Si, directly addresses this critical gap. The authors introduce two key innovations: RVBench and RagVerus. You can read the full paper here.
Introducing RVBench: A New Benchmark for Real-World Verification
To systematically explore and tackle the complexities of verifying entire software repositories, the researchers developed RVBench. This is the first verification benchmark explicitly designed for repository-level evaluation. It’s constructed from four diverse and complex open-source projects written in Verus, a language designed with verification in mind. These projects include VeriSMo (a verified security module), Anvil (for Kubernetes controller verification), IronKV (a distributed key-value store), and Vest (for high-performance parsers and serializers).
RVBench significantly scales up the complexity compared to previous function-level benchmarks. It comprises 755 proof completion tasks across 337 modules and 3,464 functions, reflecting real-world challenges like complex proof structures, inter-module lemma dependencies, and custom type definitions. The benchmark categorizes tasks into “simple” (requiring project-specific syntax but no function calls) and “complex” (requiring dependencies on other proof functions), allowing for granular evaluation of verification agents.
Beyond just size, RVBench also introduces a substantial increase in the logical reasoning complexity required. It demands reasoning about modularity, resources, temporal evolution, and concurrency – aspects crucial for real-world distributed systems and security modules.
RagVerus: A Retrieval-Augmented Approach to Proof Synthesis
To navigate the intricacies of repository-level verification, the paper introduces RagVerus, an extensible framework that combines retrieval-augmented generation (RAG) with context-aware prompting. RagVerus aims to automate proof synthesis for multi-module repositories by dynamically integrating relevant information into the LLM’s reasoning process.
The framework operates in three stages: repository indexing, retrieval, and proof generation. The repository indexing module prepares persistent indices of all code and natural language summaries derived from function metadata. This allows for efficient retrieval of relevant verification contexts, capturing both the syntax and semantic relationships within the codebase.
The retrieval module employs two complementary strategies: few-shot example retrieval and dependency retrieval. Few-shot retrieval selects representative problem-approach pairs from other verified examples to guide the LLM on correct styles and practices. Dependency retrieval identifies cross-module function signatures, premises, and type definitions necessary for proof synthesis, ensuring context awareness and premise identification.
Finally, the proof generation module synthesizes verification annotations, such as loop invariants and quantifier logic, informed by the retrieved contexts. Generated proofs are rigorously validated using the Verus compiler for logical correctness and a syntax checker for intactness, ensuring no unintended modifications to the executable code or specifications.
Also Read:
- MULocBench: A New Benchmark for Pinpointing Software Issues Beyond Code
- LLM Agents Tackle Real-World Software Compilation Challenges with BUILD-BENCH
Promising Results and Future Directions
Experimental evaluations show that RagVerus significantly improves proof pass rates. It triples proof pass rates on existing benchmarks under constrained model inference budgets and achieves a 27% relative improvement on the more challenging RVBench benchmark. This demonstrates a scalable and sample-efficient solution for automated verification.
An ablation study highlighted the critical role of intelligent retrieval. Random retrieval performed poorly, while using informalized metadata summaries for retrieval often outperformed code-only similarity, especially for tasks with similar code structures but different semantic requirements. The study also emphasized the need for a diverse, global set of examples to help LLMs learn generalizable syntax patterns.
Despite these advancements, the paper acknowledges that repository-level verification remains a significant challenge. Many complex tasks in RVBench are still unsolved, indicating a need for more specialized retrieval directions, larger context capacities, and potentially hundreds of refinement cycles for very long proofs.
Future work will focus on scaling verification beyond individual completions to handle concurrent proof synthesis across multiple interdependent modules, specializing retrieval for structural and semantic dependencies, and improving the intrinsic capabilities of LLMs for verification languages through fine-tuning and reinforcement learning.
This research marks a substantial step towards making automated formal verification a practical reality for large-scale, real-world software systems, bridging the gap between theoretical guarantees and industrial application.
