Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, percentage and fraction against Tables I to IX and the text, page and section references, quotations, the steps of techniques 1 to 4 and 7 against Sections III and IV, and the Verus forms; corrected one wrong section reference (the post-cutoff check is in Sections V-B and V-H, not Section IV), one omitted split (validation set), and marked four unmarked inferences; Verus forms are sound and already marked as inference.

source: Thompson, Saavedra, Carrott, Fisher, Sanchez-Stern, Brun, Ferreira, Lerner, First; ICSE 2025; arXiv:2412.14063v3 (28 Jan 2025), 13 pages, no appendix. Page numbers below are PDF pages.

measured, and what Coq is trusted for

Rango writes Coq proofs one tactic at a time. Before each tactic it searches the same project for finished proofs and lemma statements that look like the current goal, and puts them in the prompt of a fine-tuned 1.3 billion parameter DeepSeek-Coder model. The headline measurement is the count of benchmark theorems for which Coq accepts a generated proof within 10 minutes: 3,325 of 10,396 (32.0%), against 2,575 (24.8%) for Tactician and 2,007 (19.3%) for Proverbot9001 (Table II, p.6).

Nothing is proved about Rango itself. Coq is the only judge: Fig. 1’s caption (p.4) says “A proof attempt is correct if Coq determines that it has no errors and there are no more goals left to solve.” Inference: the theorem statements are taken from the projects as given, so whether a statement says what its author meant is outside the paper. The dataset relies on the same judge: “We applied no other filters to our data collection (e.g., stars or number of contributors), since Coq itself ensures that successfully compiled files provide sound proof data.” (Section IV, p.4)

technique 1: retrieve whole proofs by proof-state similarity, again at every step

What it is. A proof bank holds the finished proofs that the current theorem may legally see. At each step the retriever scores every banked proof by how close any of its intermediate proof states is to the current proof state, and hands the top k proofs to the model. The paper’s central claim is that this matters more than lemma retrieval.

When to use it. Inference: when a project already contains many proofs and new theorems resemble old ones, so the local proof style and the locally used lemmas carry over. The motivating example (Section II, p.2-3) is CompCert’s memval_inject_compose, proved after retrieving val_inject_compose from another file and memval_inject_incr from earlier in the same file.

Steps, from Section III-A (p.3):

1. Build the proof bank. “The proof bank consists of proofs from earlier in the file, or from one of the file’s dependencies.” Only proofs from the current project are in it.
2. Record, for each banked proof P, the proof state before each of its steps: states(P).
3. Turn a proof state into a bag of words: the words are the identifiers used in the proof state.
4. Score each banked state against the current state s with BM-25, where the documents are banked proof states and the query is s.
5. Give each proof the score of its best state: relevance(P) = max over si in states(P) of similarity(s, si).
6. Take the k highest proofs. The paper does not give k; it gives a token budget instead (technique 3).
7. Repeat steps 4 to 6 after every tactic, because the state has changed.

Verus form. Inference: Verus has no tactic-by-tactic proof state. A Verus proof is the body of a proof fn, or assert statements and loop invariant clauses inside an executable function, and the verifier answers for the whole function. The nearest thing to a proof state is the obligation that fails: the function’s requires and ensures plus the text of the failing assert, ensures or invariant clause. Inference: the bank would be the proof fn bodies, assert forall ... by blocks and loop invariants of already verified functions in the same crate, indexed by the identifiers in their requires, ensures and spec fn calls. The dependency rule carries over as: retrieve only from modules the current one imports. What does not carry over is the per-step refresh, since there are no intermediate goals to observe; the refresh point would be each verifier run that reports a new failing obligation. Inference: a Verus bank also lacks the recorded intermediate states that the max over states(P) needs, so the score would be computed on whole-function text.

Evidence. Ablation on 500 theorems drawn at random from the benchmark, each variant separately fine-tuned (Table IV, p.7): full Rango 150/500 = 30.0%; without lemmas 145/500 = 29.0%; without proofs 102/500 = 20.4%; without any retrieval 93/500 = 18.6%. 150/102 is the 47% in the abstract and 150/93 is the 61%. “Rango proves 47% more theorems than the variant without a proof retriever whereas Rango only proves 3% more theorems than the variant without a lemma retriever.” (Section V-C, p.7)

Which similarity function (Table VI, p.8, whole benchmark): BM-25 3,325/10,396 = 32.0%; TF-IDF 3,291/10,396 = 31.7%; CodeBert 125M dense embeddings with cosine similarity 2,283/10,396 = 22.0%. The paper’s reason why a retriever cannot simply be trained: “However, at training time, there is no way to know which proofs satisfy this objective.” (Section V-D, p.8)

Where it fails or what it assumes. Inference: it needs earlier proofs in the project, so the first lemmas of a new project get nothing. Inference: the CodeBert result tests one off-the-shelf embedding model that was not trained on proof states, so it does not show that dense retrieval in general is worse. Success still falls steeply with the length of the human proof for all three tools (Fig. 5, p.9), and falls for files with a hundred or more dependencies (Fig. 6, p.9).

technique 2: retrieve lemma statements with TF-IDF

What it is. A second retriever returns statements, without proofs, of lemmas that the next tactic could cite.

Steps, from Section III-B (p.3):

1. Build the lemma bank: “the set of lemmas appearing earlier in the current file, or in one of the file’s dependencies”, current project only.
2. Treat each lemma statement as a document whose words are its identifiers, and the current proof state as the query.
3. Score with TF-IDF and keep the j best. The paper does not give j.

When to use it. When the model would otherwise have to guess lemma names. Without retrieval a tool has to guess that a lemma such as val_inject_compose exists; the paper adds: “However, Rango does not have to rely on luck because it can retrieve relevant lemmas and proofs.” (Section II, p.3) The worked case is swap_cmpu_bool in CompCert’s Values.v, a file with 300 dependencies, where the found proof uses Int.swap_cmpu, which is defined in another file and not used earlier in Values.v (Section V-G, p.9).

Verus form. Inference: the documents would be the signatures of proof fn lemmas, meaning name, parameters, requires and ensures, taken from the crate and from the vstd modules it imports; the query would be the failing obligation. The standard library is a difference: Rango’s bank excludes everything outside the project, while a Verus proof often needs a vstd lemma, so the bank has to include it. Lemmas already published through broadcast proof need no call and therefore no retrieval.

Evidence. Small on its own: 150 against 145 of 500 (Table IV). On a second sample of 500 (Table V, p.7, CoqStoq split column) the gap is one theorem, 160 against 159. Inference: a difference of 1 to 5 theorems out of 500 from a single run with temperature 1.0 is within what sampling noise could produce; the paper reports no repeated runs.

technique 3: build fine-tuning examples exactly as the prompt is built at inference, with a fixed token budget per part

What it is. The model is fine-tuned on (prompt, next tactic) pairs in which the prompt already contains retrieved proofs and lemmas, so the model learns to use retrieved material instead of memorising one project.

Steps, from Sections III-C (p.4) and V-A (p.5-6):

1. For every proof step in the training projects, run both retrievers as they would run at inference. “We create each training example exactly as we would during inference.”
2. Assemble four inputs: retrieved proofs, retrieved lemmas, theorem statement with the proof script so far, current proof state. The target is the next tactic.
3. Give each part its own budget: 1,024 tokens for proofs, 512 for lemmas, 512 for theorem and script, 1,024 for the proof state, 128 for the output.
4. Truncate each part by its own rule: keep the largest whole number of proofs that fits, the same for lemmas, the longest suffix of the theorem and script, the longest suffix of the proof state, and at training time the longest prefix of the output.
5. Compute the loss on the target tokens only.
6. Fine-tune DeepSeek-Coder 1.3B with LoRA for 60,000 steps at effective batch size 32, Adam, learning rate 10^-3, and keep the checkpoint with the best validation loss.

When to use it. Inference: whenever a retrieval-augmented prover is trained instead of prompted. Each ablation variant in the paper was retrained without the removed retriever, so the comparisons are between models that each saw their own prompt format in training.

Verus form. Inference: the four parts map to retrieved verified functions, retrieved lemma signatures, the function under proof with its current annotations, and the verifier’s error text. The suffix rule for the script assumes the newest tactics matter most; for a Verus function the signature with requires and ensures sits at the top, so a suffix cut would drop the contract. A Verus prompt would have to keep the signature and cut the middle of the body.

Evidence that retrieval stands in for training on the project (Table V, p.7). The authors retrained every variant on a split made by file, so that the weights have seen other files of the test projects, and compared on 500 theorems that are test items under both splits. Project split against file split: Rango 160 against 184 of 500; without lemmas 159 against 177; without proofs 111 against 140; without retrieval 89 against 127. The variants that lack proof retrieval gain 26% and 43% from having the project in their weights; those that have it gain 15% and 11%. “This indicates that Rango’s proof retriever captures a significant amount of the information that would be gained by training directly on files from the current project.” (Section V-C, p.7)

Limits. Inference: this evidence is for a small fine-tuned model. The paper does not test whether a large general model that is only prompted gets the same gain from retrieved proofs.

technique 4: rollout search

What it is. A proof search with no tree and no memory. Sample a tactic, check it, keep going until the proof closes or a tactic fails, then start over from the theorem.

Steps, from Section III-D (p.4):

1. Start a rollout from the empty proof.
2. Sample one tactic from the tactic generator with temperature sampling (temperature 1.0, Section V-A).
3. Append it and have Coq check the attempt, which is then complete, invalid or incomplete.
4. Complete: stop with success. Invalid: “the tactic sampled from the language model resulted in an error, and the searcher begins a new rollout.” Incomplete: go to step 2.
5. Repeat until success or the 10 minute timeout.

Evidence (Table VIII, p.8, ablation set): rollout 150/500 = 30.0%; best-first search with beam decoding 142/500 = 28.4%; best-first search with temperature sampling 125/500 = 25.0%. Both best-first variants expand b = 4 tactics per step and drop invalid and redundant candidates (Section V-F, p.9).

Stated weakness: “One weakness of the rollout search is that it does not use previous proof attempts to inform subsequent proof attempts.” (Section V-F, p.8)

Verus form. Inference: rollout needs a checker that accepts a partial proof and reports it as incomplete, which Coq does per tactic. Verus gives a per-function verdict with a list of failing obligations, so the nearest loop is: sample a whole annotated function, verify, and on failure either resample from scratch (a new rollout) or continue from the candidate with the errors in the prompt. The paper’s result favours cheap restarts over a scored frontier when each check is fast; a Verus check is slower than one Coq tactic, so the trade may differ.

technique 5: prefix retrieval, and alternating two retrievers across rollouts

What it is. Rango-PRE replaces both retrievers with the lines of the file directly above the theorem, which is what Baldur did. Rango-Hybrid “simply alternates between rollouts using Rango and Rango-PRE” (Section V-E, p.8).

When to use it. The authors’ hypothesis: prefix context wins when what is needed sits just above the theorem, because it is shown as originally written; retrieval wins when what is needed is elsewhere in the project. That is offered as a hypothesis, and the paper does not test it directly.

Evidence (Table VII, p.8). CoqStoq benchmark: Rango 3,325/10,396 = 32.0%; Rango-PRE 3,259/10,396 = 31.3%; Rango-Hybrid 3,478/10,396 = 33.5%. Post-cutoff projects: 352/1,171 = 30.1%; 350/1,171 = 29.9%; 380/1,171 = 32.5%.

Verus form. Inference: prefix retrieval is free in Verus, it is the rest of the file above the function. The hybrid is two prompt builders used on alternate attempts, with no change to the verifier.

Inference: this table weakens the headline. The simplest baseline is 66 theorems (0.7 percentage points) behind full Rango on the benchmark and 2 theorems behind on the post-cutoff projects. The 47% gain of technique 1 is measured against a model with no project context at all, not against a model that sees the file prefix.

technique 6: run several provers and take the union

Steps and evidence (Table II last row, p.6): run a second tool on the same theorems and count a theorem proved if either tool proves it. Rango with Tactician 3,866/10,396 = 37.2%; with Proverbot 3,724/10,396 = 35.8%; with Graph2Tac 319/496 = 64.3%, against 276/496 for Rango alone. The paper’s observation is that “each tool finds proofs for a significant subset of theorems where Rango could not find a proof” (Section V-B, p.6).

Verus form. Inference: any two proof generators can be combined this way because the verifier makes acceptance cheap and safe; the cost is the sum of both budgets, which the paper does not charge for when it reports the union.

technique 7: a benchmark split that tests transfer to unseen projects, plus a post-cutoff check

Steps, from Section IV (p.4-5):

1. Collect every GitHub repository whose primary language was Coq on 5 November 2023, with no popularity filter.
2. Compile with the Makefile or in _CoqProject order under Coq 8.18; validate each file with CoqPyt; keep repositories with at least one valid file.
3. For each proof step store its text, its proof state and the premises it uses, and the premises available at each point of the file.
4. Split by project, not by file: the benchmark is the CoqGym projects that compile in Coq 8.18, plus CompCert, plus long-maintained Coq-Community projects (the validation set also draws on Coq-Community); every project in neither is training.
5. Remove from training every file with a theorem statement that exactly matches one in validation or benchmark.
6. Not in Section IV, but in Sections V-B (p.6) and V-H (p.10): because the benchmark projects predate the base model’s pretraining cutoff, also test on two projects first committed after it (Coq-BB5, PnVRocqLib).

Sizes (Table I, p.5): 2,208 training repositories with 181,562 theorems and 2,008,543 steps; 12 benchmark repositories with 10,396 theorems and 162,989 steps; 6 validation repositories with 4,971 theorems and 53,983 steps.

Verus form. Inference: the recipe transfers as: split by crate, deduplicate by exact function signature and contract, and hold out crates created after the model’s cutoff. A Verus corpus of this size does not exist; the paper’s 2,226 repositories took no curation only because Coq’s check made every compiled file trustworthy, and the same argument holds for any file that Verus verifies without assume or external_body holes.

Evidence from the post-cutoff check (Table III, p.6): Rango 352/1,171 = 30.1%, Tactician 331/1,171 = 28.3%, Proverbot 217/1,171 = 18.5%. On PnVRocqLib alone Tactician is ahead, 168 against 166 of 688.

numbers that do not add up, and things to read with care

• Edit distance. The text says Rango’s proofs are “12 edit operations closer to human-written proofs than Tactician, and 21 edit operations closer to human-written proofs than Proverbot” (Section V-G, p.10). Table IX (p.10) gives means of 39.7, 52.8 and 61.2 over the 1,252 theorems all three tools proved, so the differences are 13.1 and 21.5.
• The margin over Tactician shrinks from 29% on the benchmark (3,325 against 2,575) to 6% on post-cutoff projects (352 against 331). The paper names pretraining contamination as a threat (Section V-H, p.10). Inference: the two projects also differ in kind from the benchmark, so the drop cannot be assigned to contamination alone.
• Graph2Tac is compared on 3 projects and 496 theorems, under a different Coq version (8.11 against 8.18), matching theorems by exact statement: 276 against 265. On PolTac Graph2Tac is ahead, 138 against 127 of 152 (Table II, p.6). The abstract’s “29% more theorems than the prior state-of-the-art tool Tactician” does not mention that the closer competitor is 4% behind on a subset.
• Inference: CompCert supplies 6,091 of the 10,396 benchmark theorems (59%), so the total is mostly a CompCert result. Rango’s rate there is 1,977/6,091 = 32.5%.
• Hardware differs: Rango and Graph2Tac ran with a GPU, Tactician and Proverbot on one CPU, all with a 10 minute limit, and Proverbot stops at a depth limit, usually earlier (Section V-B, p.6).
• The 4% for the hybrid is 3,478/3,325 = 1.046.

already done, which VL should not redo

• Whether in-project proofs help a step-wise prover: measured here, with retrained ablations.
• BM-25 against TF-IDF against one dense embedding for proof retrieval: measured on 10,396 theorems; the two sparse methods are 34 theorems apart.
• Rollout against best-first search for a small tactic model: measured on 500 theorems.
• Inference: what is not done, and would be new for Verus, is the same comparison for SMT-based proofs, where there is no per-step state, and against a strong prompted model that sees the file prefix.

threat to VeruLaw

Inference: low as a competitor, useful as a method. Rango targets Coq tactic proofs with given theorem statements; it writes no code and no specifications, and it does not address Rust. Its transferable result is that the cheapest project-aware context (the file prefix, or sparse retrieval over the project’s own proofs) buys most of the gain, and any team building a Verus agent can add that in days. So it lowers the barrier for others as much as for VL.

techniques for the catalog

• proof retrieval by state similarity: score each finished in-project proof by the best BM-25 match between any of its intermediate proof states and the current one, and put the top proofs in the prompt.
• per-step retrieval refresh: rerun retrieval after every proof step because the goal has changed.
• identifier bag-of-words for proof text: use only the identifiers of a goal or lemma as the words for sparse retrieval.
• lemma statement retrieval: rank earlier in-project lemma statements by TF-IDF against the current goal so the model cites real names.
• train-as-inference prompts: build each fine-tuning example by running the retrievers exactly as at inference, with a fixed token budget and truncation rule per prompt part.
• rollout search: sample one step at a time, restart from the theorem on the first error, and never keep a frontier.
• prefix retrieval: use the file text directly above the theorem as the only context.
• alternating-retriever rollouts: switch between two context builders on successive attempts to cover both nearby and far context.
• prover union: run complementary provers and accept a proof from any of them.
• project-level split with post-cutoff check: hold out whole projects, drop training files with matching theorem statements, and retest on projects newer than the model’s cutoff.
• file-split against project-split comparison: retrain on a by-file split to measure how much of the project knowledge retrieval already supplies.

Last edited: 2026-10-13