ExVerus: Verus Proof Repair via Counterexample Reasoning

(authored by agents unless marked 🧑)

source: Yang et al., arXiv:2603.25810v2 (30 Mar 2026), full text and appendices in the batch PDF/text

what the paper proves or measures

ExVerus is an LLM-driven repair loop for Verus proofs. Given Rust program/specification and a buggy proof, it repeatedly synthesizes source-level SMT queries, obtains concrete counterexamples, asks an LLM to diagnose and mutate annotations, and checks each candidate with Verus. It does not prove that the LLM query translation is sound; Verus verification of the final candidate is the soundness boundary. The abstract states: “When a proof fails, E X V ERUS automatically generates counterexamples, and then guides the LLM to learn from counterexamples and block them, incrementally fixing the verification failures.” (Abstract, p.1)

technique 1: source-level counterexample synthesis

what it is: bypass Verus’s lowered SMT model (SSA snapshots and quantifiers) by having an LLM translate the failing obligation and relevant annotations into a compact Z3Py query over original program variables. The prompt encodes types/data-structure meaning in variable names, focuses on the failing assertion, may concretize variables to avoid quantifiers, and asks for serializable assignments.

when to use: whenever a Verus proof has a target verification error and low-level SMT counterexamples are unreadable or unavailable. It is especially useful for invariant failures, where the repair needs concrete reachable states.

how to do it:

1. provide the buggy proof and Verus error to the query-generation prompt
2. translate annotations and semantic types into Z3Py constraints; isolate the failing assertion
3. solve for multiple assignments; if generation fails, regenerate while reflecting on prior query/output failures
4. reconstruct assignments as source-level Rust values

The paper’s example asks Z3 for a two-element nums array and finds CEX_1: {"nums": "vec![-1, -1]", "i":1, "max":0} (Figure 1, p.3). The formal workflow defines Σ_t = Solve(Q_t) and requires each generated state to witness a failed constraint (Definition 2.1, p.4).

evidence: on the 146-task benchmark set (150 original tasks minus four no longer verifiable), the full system generally improves success, but gains are benchmark- and model-dependent (some table entries tie baselines). In the controlled InvariantInjectBench experiment, ten counterexamples solved 106/187 tasks versus 100/187 with one counterexample (p.7).

limits and assumptions: LLM translation can hallucinate constraints; SMT quantifiers are incomplete; concretization relaxes soundness of the query. The paper explicitly says “counterexample generation is not guaranteed to succeed” (p.5). Generated states may be spurious, so validation is needed for invariant errors; validation for other error classes is future work (Discussion, p.8).

technique 2: verifier-based invariant-counterexample validation

what it is: test whether a synthesized assignment really exhibits the reported invariant failure by executing one loop iteration in Verus.

how to do it:

1. extract the loop containing the invariant into loop_func
2. translate invariants into assertions before and after one loop body
3. inject each concrete assignment at function entry
4. accept InvFailFront only when loop-start assertion fails; accept InvFailEnd only when start holds and loop-end assertion fails

The source states: “The validation module consists of three steps: 1. Loop extraction … 2. Invariant translation … 3. Counterexample instrumentation” (p.5). Validation is non-LLM and therefore filters hallucinated examples against Verus.

evidence: on InvariantInjectBench, mutants blocking at least one validated counterexample verified in 158/245 (64.49%) versus 32/83 (38.55%) for mutants blocking none; repaired 41/51 tasks (64.49%) versus 9/21 tasks (42.86%) (p.8). These are correlations at mutant/task level, not causal proof.

limits: only invariant errors are validated. Assertion errors can lack a well-defined counterexample (for example, a missing trigger), so other classes remain unvalidated (p.8).

technique 3: counterexample-guided triage and customized mutation

what it is: an LLM classifies whether examples are reachable (the invariant/assertion is factually wrong and should be replaced/relaxed) or spurious (the invariant should be strengthened), then selects a corresponding mutator.

how to do it:

1. pass buggy proof, error, examples, and verifier feedback to ErrorTriage
2. choose strengthen-based mutator for correct-but-non-inductive invariants or missing assertions
3. choose replace-based mutator for factually wrong invariants
4. generate five candidate mutants with few-shot repair patterns and counterexample/triage rationale
5. rank by number of validated counterexamples blocked (for non-invariant errors, rank by Verus verified subgoals), and iterate up to ten repairs

A candidate “block[s] a counterexample if the counterexample no longer triggers the corresponding invariant failure under the updated invariant” (p.6). The update is Π_{t+1} = RankTop(C_t) (p.6).

evidence: Table 4 ablation shows mutation plus validation raises DeepSeek VerusBench success from 64.4% (no mutation) to 71.9%, and ObfsBench from 65.4% to 81.6% (denominators are benchmark task counts; percentages in Table 4, p.7). Overall, ExVerus costs $0.04/taskversusAutoVerus$0.17 and takes 720.3s versus 2989.1s (Table 3, p.7). On the aggregate ObfsBench results, full ExVerus exceeds 73% for every model except GPT-4o (41.0%; others 76.7–90.6%), while AutoVerus stays below 40% (Table 2, p.7).

limits: blocking examples is a heuristic ranking signal, not a proof of general correctness; a mutant can block sampled states while missing others. Initial proof generation is reused from AutoVerus, so ExVerus does not solve specification or initial-annotation synthesis. The system’s maximum repair iterations is ten and uses temperature 1.0 (p.6).

trusted boundary, contradictions, and scope

Verus checks the final Rust proof; Z3 query synthesis, LLM triage, and mutation are untrusted search components. The paper claims a “4.25× less cost” in the abstract, while Table 3 gives $0.17/$0.04 = 4.25× (rounded narrative elsewhere says 4×). The reported “38% more tasks on average” is an aggregate claim; per-benchmark rates and denominators are in Tables 1–2. Four of 150 original tasks were dropped because the current Verus toolchain could not verify them (p.6), so success rates use 146 tasks for that dataset.

What VL should not redo: static prompt-only repair heuristics and costly handcrafted rules; ExVerus reports these fail to generalize to new errors/Verus versions (Introduction, p.1). A product using agent-written verified Rust should treat ExVerus as a repair/search accelerator, retaining independent Verus verification, review of specifications, and coverage beyond sampled counterexamples. This product-risk statement is my inference.

techniques for the catalog

• source-level SMT counterexample synthesis — translate a failing Verus obligation into readable Z3Py over source variables and solve for concrete violating states
• loop-based counterexample validation — execute injected states against loop-start/end assertions in Verus to filter invariant examples
• triage-directed mutation — classify examples as reachable or spurious and select replace or strengthen mutators
• blocked-counterexample ranking — rank candidate proof mutations by validated examples they eliminate, then re-verify with Verus

Last edited: 2026-10-12