Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Repository-Level Program Verification with Large Language Models

Si Cheng Zhong, Xujie Si

TL;DR

This paper addresses the challenge of repository-level formal verification by introducing RVBench, a benchmark built from four Verus-based projects to capture cross-module dependencies and environmental interactions, and RagVerus, a retrieval-augmented framework that injects repository context and premises into LLM-based proof synthesis. RagVerus integrates repository indexing, few-shot and dependency retrieval, and proof generation with rigorous verification through the Verus compiler and Lynette, achieving a 27% relative improvement on RVBench and notable gains on function-level tasks. The work highlights both the potential of context-aware retrieval to scale verification and the remaining gaps in handling complex, multi-module proofs, suggesting directions for richer premise pools and specialized retrieval strategies. Overall, RVBench and RagVerus lay a scalable foundation for automated, real-world verification of large codebases, with implications for higher assurance software systems.

Abstract

Recent advancements in large language models (LLMs) suggest great promises in code and proof generations. However, scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are crucial challenges overlooked by existing LLM-based methods with a special focus on targeting isolated, function-level verification tasks. To systematically explore and address the significant challenges of verifying entire software repositories, we introduce RVBench, the first verification benchmark explicitly designed for repository-level evaluation, constructed from four diverse and complex open-source Verus projects. We further introduce RagVerus, an extensible framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories. RagVerus triples proof pass rates on existing benchmarks under constrained model inference budgets, and achieves a 27% relative improvement on the more challenging RVBench benchmark, demonstrating a scalable and sample-efficient verification solution.

Towards Repository-Level Program Verification with Large Language Models

TL;DR

This paper addresses the challenge of repository-level formal verification by introducing RVBench, a benchmark built from four Verus-based projects to capture cross-module dependencies and environmental interactions, and RagVerus, a retrieval-augmented framework that injects repository context and premises into LLM-based proof synthesis. RagVerus integrates repository indexing, few-shot and dependency retrieval, and proof generation with rigorous verification through the Verus compiler and Lynette, achieving a 27% relative improvement on RVBench and notable gains on function-level tasks. The work highlights both the potential of context-aware retrieval to scale verification and the remaining gaps in handling complex, multi-module proofs, suggesting directions for richer premise pools and specialized retrieval strategies. Overall, RVBench and RagVerus lay a scalable foundation for automated, real-world verification of large codebases, with implications for higher assurance software systems.

Abstract

Recent advancements in large language models (LLMs) suggest great promises in code and proof generations. However, scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are crucial challenges overlooked by existing LLM-based methods with a special focus on targeting isolated, function-level verification tasks. To systematically explore and address the significant challenges of verifying entire software repositories, we introduce RVBench, the first verification benchmark explicitly designed for repository-level evaluation, constructed from four diverse and complex open-source Verus projects. We further introduce RagVerus, an extensible framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories. RagVerus triples proof pass rates on existing benchmarks under constrained model inference budgets, and achieves a 27% relative improvement on the more challenging RVBench benchmark, demonstrating a scalable and sample-efficient verification solution.

Paper Structure

This paper contains 33 sections, 4 figures, 6 tables.

Table of Contents

  1. Introduction
  2. Background
  3. The Verus Verifier
  4. Large Language Models (LLMs) in Verification
  5. RVBench: Creating A New Repository-level Verification Benchmark
  6. Benchmark Construction and Scope
  7. Benchmark Creation Methodology
  8. Task Identification
  9. Metadata Extraction
  10. Proof Completion Tasks
  11. Evaluation Metrics
  12. RagVerus Framework
  13. Repository Indexing
  14. Retrieving Useful Contexts for Repository-level Verification
  15. Few-Shot Example Retrieval
  16. ...and 18 more sections

Figures (4)

  • Figure 1: An annotated Verus function with spec in yellow and proof in orange. Note that each code mode can have function calls requiring dependency resolution from other sources.
  • Figure 2: The RagVerus pipeline consists of three stages: 1) mining code properties, 2) retrieving task-specific information, and 3) generating proofs for verifiable code
  • Figure 3: Comparison of metadata summaries for condm.rs (left) and ms1.rs (right), where the informalized summaries explicitly identify the logic differences and the key objects being operated on.
  • Figure 4: Code informalization summarizes the code functionalities. Here, one can identify through the summaries that is_locked is a good helper candidate for the task add_element.