# RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation

arXiv: https://arxiv.org/abs/2502.05344 · HTML: https://mlsanity.com/paper/2502.05344/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in RAG for code, one of 15 directions in Retrieval-augmented generation.
- Builds on 16 of its 33 references that are in the map.
- First posted on arXiv 7 Feb 2025.

## Placed in

- Retrieval-augmented generation / [RAG for code](https://mlsanity.com/rag/rag-for-code/)

## Builds on (most cited first, 16 of 16)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Billion-scale similarity search with GPUs](https://mlsanity.com/paper/1702.08734/) (2017)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Repository-Level Prompt Generation for Large Language Models of Code](https://mlsanity.com/paper/2206.12839/) (2022)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://mlsanity.com/paper/2405.01787/) (2024)
- [Selene: Pioneering Automated Proof in Software Verification](https://mlsanity.com/paper/2401.07663/) (2024)
- [Guiding Enumerative Program Synthesis with Large Language Models](https://mlsanity.com/paper/2403.03997/) (2024)

## Built on by (most cited first, 4 of 4)

- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [ExVerus: Verus Proof Repair via Counterexample Reasoning](https://mlsanity.com/paper/2603.25810/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [Second-Order Problem Solving for Recursive Self-Improvement in Formal Verification](https://mlsanity.com/paper/2610.05701/) (2026)

## Abstract (arXiv)

Scaling automated formal verification to real-world projects requires resolving cross-module dependencies and global contexts, which are challenges overlooked by existing function-centric methods. We introduce RagVerus, a framework that synergizes retrieval-augmented generation with context-aware prompting to automate proof synthesis for multi-module repositories, achieving a 27% relative improvement on our novel RepoVBench benchmark -- the first repository-level dataset for Verus with 383 proof completion tasks. RagVerus triples proof pass rates on existing benchmarks under constrained language model budgets, demonstrating a scalable and sample-efficient verification.