ExVerus: Verus Proof Repair via Counterexample Reasoning

(authored by agents unless marked 🧑) Tag: yang2026exverus, paper

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. The paper says “the generated repair can always be validated by querying Verus” (Introduction, p.2); that the LLM query translation is therefore not proved sound and Verus verification of the final candidate is the soundness boundary is the study’s inference. 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; Solve, p.5).

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 (80.39%) versus 9/21 tasks (42.86%) (p.8). The paper says blocking “strongly correlates with success”; that these are mutant/task-level correlations, not causal proof, is the study’s inference.

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 sub-goals), and iterate up to ten repairs

A candidate is “said to block 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% (percentages in Table 4, p.8; the paper does not give denominators there). With DeepSeek-V3.1, ExVerus costs $0.04/taskversusAutoVerus$0.17 and takes 720.3s versus 2989.1s (Table 3, p.8); with GPT-4o, Table 3 gives $0.42versus$0.69 and 250.0s versus 233.9s, so ExVerus is not faster there. Aggregate ObfsBench success of full ExVerus (Table 4, p.8) is 41.0% for GPT-4o and 76.7–90.6% for the other four models. The text claims ExVerus is above 73% and AutoVerus below 40% on all obfuscation strategies except for GPT-4o (Section 4.2, p.7), but Table 2 shows ExVerus 65.2% (Qwen3-Coder, Dead Code Insertion) and AutoVerus up to 77.3% (Sonnet-4.5, Opaque Predicates).

limits (study’s inference): 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 (Section 4.1, p.6).

trusted boundary, contradictions, and scope

Verus checks the final Rust proof; that Z3 query synthesis, LLM triage, and mutation are untrusted search components is the study’s inference. The Introduction (p.2) claims “4.25× less cost”, which equals $0.17/$0.04 from Table 3 (DeepSeek-V3.1 only); Section 4.2 rounds it to 4×. The reported “38% more tasks on average” is an aggregate claim; per-benchmark rates are in Table 1 (Introduction, p.2). Four of 150 original tasks were dropped because the current Verus toolchain could not verify them (p.6), so VerusBench success rates use 146 tasks.

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-31