# Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

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

## Key facts

- Cited by 27 papers in the map (data through 14 Oct 2026).
- Placed in Agentic RAG, agents and memory, one of 15 directions in Retrieval-augmented generation.
- Builds on 47 of its 101 references that are in the map.
- First posted on arXiv 18 Dec 2024.

## Placed in

- Retrieval-augmented generation / [Agentic RAG, agents and memory](https://mlsanity.com/rag/agentic-rag-agents-and-memory/)

## Builds on (most cited first, 30 of 47)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [PaLM: Scaling Language Modeling with Pathways](https://mlsanity.com/paper/2204.02311/) (2022)
- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [CodeBERT: A Pre-Trained Model for Programming and Natural Languages](https://mlsanity.com/paper/2002.08155/) (2020)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Benchmarking Large Language Models in Retrieval-Augmented Generation](https://mlsanity.com/paper/2309.01431/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Retrieval Augmented Code Generation and Summarization](https://mlsanity.com/paper/2108.11601/) (2021)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Fairness Testing: Testing Software for Discrimination](https://mlsanity.com/paper/1709.03221/) (2017)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [TBar: Revisiting Template-based Automated Program Repair](https://mlsanity.com/paper/1903.08409/) (2019)
- [A Syntax-Guided Edit Decoder for Neural Program Repair](https://mlsanity.com/paper/2106.08253/) (2021)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [RAP-Gen: Retrieval-Augmented Patch Generation with CodeT5 for Automatic Program Repair](https://mlsanity.com/paper/2309.06057/) (2023)

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

- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://mlsanity.com/paper/2603.19329/) (2026)
- [DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems](https://mlsanity.com/paper/2510.10815/) (2025)
- [VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean](https://mlsanity.com/paper/2602.18307/) (2026)
- [Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry](https://mlsanity.com/paper/2505.14479/) (2025)
- [Agentic Verification of Software Systems](https://mlsanity.com/paper/2511.17330/) (2025)
- [MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study](https://mlsanity.com/paper/2503.04763/) (2025)
- [RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation](https://mlsanity.com/paper/2505.22846/) (2025)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Automated Lemma Discovery in Agentic Program Verification](https://mlsanity.com/paper/2603.22114/) (2026)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [Vero: Can AI Agents Build Formally Verified Software Repositories?](https://mlsanity.com/paper/2608.13522/) (2026)
- [Neuro-Symbolic Proof Generation for Scaling Systems Software Verification](https://mlsanity.com/paper/2603.19715/) (2026)
- [On Reasoning-Centric LLM-based Automated Theorem Proving](https://mlsanity.com/paper/2604.19558/) (2026)
- [Harnessing Code Agents for Automatic Software Verification](https://mlsanity.com/paper/2607.06341/) (2026)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Skills for the future software profession: beyond agentic AI!](https://mlsanity.com/paper/2606.21894/) (2026)
- [An Empirical Study of LLM-Generated Specifications for VeriFast](https://mlsanity.com/paper/2606.26490/) (2026)
- [Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study](https://mlsanity.com/paper/2608.05420/) (2026)
- [PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs](https://mlsanity.com/paper/2608.12762/) (2026)
- [ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents](https://mlsanity.com/paper/2610.03796/) (2026)
- [Let the Library Speak: Self-Advertised Method Selection for Formal Proving](https://mlsanity.com/paper/2610.09401/) (2026)

## Abstract (arXiv)

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the-art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven.