mlsanityData to 14 Oct 2026

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

arXiv 2502.05344 ↗First posted 7 Feb 2025cs.SE cs.AIcited by 4

On the map: Retrieval-augmented generation → RAG for code

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.

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.

Builds on

16 of 33 references.

References · 16

  1. 2020Language Models are Few-Shot Learnerscited by 32,419
  2. 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,297
  3. 2017Billion-scale similarity search with GPUscited by 2,497
  4. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  5. 2022Repository-Level Prompt Generation for Large Language Models of Codecited by 106
  6. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  7. 2024Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verificationcited by 58
  8. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  9. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 53
  10. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
  11. 2023Finding Inductive Loop Invariants using Large Language Modelscited by 36
  12. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 35
4 more
  1. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 33
  2. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 20
  3. 2024Selene: Pioneering Automated Proof in Software Verificationcited by 12
  4. 2024Guiding Enumerative Program Synthesis with Large Language Modelscited by 9

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 4.

4 papers.

  1. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  2. 2026ExVerus: Verus Proof Repair via Counterexample Reasoningcited by 3
  3. 2026VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generationcited by 3
  4. 2026Second-Order Problem Solving for Recursive Self-Improvement in Formal Verificationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Towards Repository-Level Program Verification with Large Language Models
  2. 2026KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code
  3. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
  4. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
  5. 2026P3: Joint Program-and-Proof Planning for Verified Code Generation
  6. 2026Automating Formal Verification with Reinforcement Learning and Recursive Inference
  7. 2026RepoZero: Can LLMs Generate a Code Repository from Scratch?
  8. 2026Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set