F-IDEs with Features and VCs Designed to Assist Human Reasoning When Verification Fails

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

scope and contribution

The paper presents two formalization integrated development environments (F-IDEs) for RESOLVE: a long-running browser IDE and RESOLVE Studio, a JetBrains-based desktop IDE. The stated goal is to make failed verification useful to people by exposing understandable verification conditions (VCs). The authors write, “The first environment, referred to as the web-IDE, has been used for several years to teach aspects of formal specification and verification, including why and where verification conditions (VCs) arise and how to use them when verification fails” (abstract, p. 51). They also report that RESOLVE has reached “Over 25,000 students across multiple institutions” (section 2, p. 52). The central technical contribution is a sequent VC generator that removes irrelevant assumptions while preserving proof-relevant context.

Inference: The transferable lesson for Verus is that verifier UX is part of the proof method: a failed obligation must be linked to source code, shown with a small context, and explorable at the rule level. RESOLVE is a different language and prover, so the Verus mapping below is an engineering inference.

technique 1: syntax-directed sequent VC generation

What it is. RESOLVE first turns source into assertive code (Assume, Confirm, Stipulate, assignments, and calls), then eliminates statements backwards with proof rules. Each final VC is a Gentzen sequent with antecedent and succedent sets; standard sequent reductions split conjunctions/disjunctions until atomic formulas. The paper states, “Generation of VCs that are both necessary and sufficient in order to prove that an implementation is correct w.r.t. its specification is a syntax-directed process” (section 4, p. 55).

When to use it. Use this pipeline when a language has contracts, loops, calls, and theory lemmas and users need a source-to-obligation explanation. It is useful both for automatic proving and for teaching why an obligation exists.

How to do it.

1. Preprocess code into assertive-code blocks, making mathematical assertions explicit (section 4, p. 55).
2. Represent the final Confirm as a conjunction of Gentzen sequents Γ ⊢ Δ; the paper defines antecedent and succedent sets and their disjunctive interpretation (section 4.2, pp. 56–57).
3. Start at the statement immediately before the final confirmation and apply its proof rule; continue backwards one statement at a time (section 4.3, p. 57).
4. After each statement rule, apply sequent reductions, equality handling, and theory rewrites (section 4.3, p. 57).
5. Split the resulting conjunction into individual sequents and send each to the congruence-closure prover or another backend (section 4.3, p. 57).

Verus form. Inference: Verus already lowers Rust specifications to SMT obligations, so a direct reimplementation is unnecessary. A Verus-facing diagnostic layer could retain an obligation provenance record for each requires, ensures, assert, loop invariant, and proof assert, then show the corresponding SMT goal and assumptions. Verus uses requires, ensures, invariant, assert, assert forall, assume, old, and recommends; it does not use RESOLVE’s Confirm or Gentzen syntax. Inference: preserving the original Rust/Verus construct in each diagnostic avoids the IVL impedance mismatch the paper identifies in related work.

Evidence and limits. The method is presented as a design and implemented in RESOLVE; no soundness denominator beyond the necessary-and-sufficient design claim is supplied. The backend can be an in-house prover, specialized decision procedures, or SMT. Inference: applicability to Verus depends on exposing its internal obligation provenance, which this paper does not measure.

technique 2: parsimonious assumptions using free-variable closure

What it is. A conventional rule adds every conjunct of an encountered assumption to every VC. The revised rule adds a conjunct only when its variables can affect the sequent, while a transitive free-variable closure preserves bridge facts. The paper says, “The key to the new parsimonious rule, however, is to only add givens that are ‘relevant’ to a given sequent” (section 5, p. 58).

When to use it. Use it when contracts or module constraints create large contexts and users must understand why a failed VC fails. Do not apply plain variable-overlap filtering when one fact connects the goal to another fact through a chain of equalities or predicates.

How to do it.

1. Split an Assume ϕ formula into conjuncts ⟨⟨ϕ⟩⟩ (section 5, p. 58).
2. For each current sequent s, compute its specification free variables SFV.
3. Compute FVC (free-variable closure) of each conjunct over the conjunct list; this transitively includes clauses sharing variables (example 5.2, p. 59).
4. Add the conjunct to s only when FVC(conjunct) intersects SFV of the sequent; otherwise leave s unchanged (parsimonious assume rule, p. 58).
5. Apply equality substitution and sequent simplification after statement elimination (postprocessing rule, pp. 59–60).

The paper’s example assumes p(c) ∧ c = b ∧ s = x and confirms p(b). Plain overlap would discard p(c) before seeing c = b; closure keeps both. The paper gives the exact result, “FVC( p(bv ), hhp(cv ), cv = bv , … ii ) = {cv , bv }” (example 5.2, p. 59).

Verus form. Inference: implement this as a diagnostic context slicer over Verus trigger terms and specification variables, not as a change to the trusted proof kernel. Keep assumptions that share variables transitively through equalities, quantified predicates, or function applications. Display the sliced context while sending the original full context to Verus, or prove that the slice is equivalent before using it for proving. Verus code would continue to use assert, assume, requires, ensures, and loop invariant; there is no Verus modifies clause or invariant(...) call.

Evidence. Table 1 reports five operation families. Non-parsimonious contexts contain ten or more antecedents in every VC; parsimonious contexts have, respectively, 0, 0, 0, 0, and 0 VCs with ten or more antecedents for List Search (35 VCs), List Reverse (8), Queue Append (8), Queue Selection Sort (36), and Stack Copy (24) (table 1, p. 63; the sentence on p. 64 says none contain more than ten, while the table’s #VCsA≥10 column is zero). For #VCsA≥5, the parsimonious counts are 16/35, 0/8, 0/8, 16/36, and 5/24. Inference: these are context-size measurements, not proof-success rates or user-study effect sizes.

technique 3: equality folding and contradiction-aware stipulation

What it is. After assumptions are selected, top-level equalities v = t are substituted throughout antecedents and goals. Control predicates from conditionals and loops are inserted with Stipulate, which is retained even when variable overlap would otherwise remove it. This preserves detection of contradictory, unreachable paths.

How to do it.

1. Eliminate statement rules and apply the parsimonious assume rule.
2. For each top-level antecedent equality v = t, substitute t for v in all antecedents and succedents (ApplyEqLeft, section 5, pp. 59–60).
3. For every branch predicate generated from if/while, add it with Stipulate, regardless of overlap (section 5, pp. 60–61).
4. Report a vacuously true or contradictory sequent instead of timing out. The paper explains, “Since there are no overlaps between the assumed clauses and the final confirm, each would be discarded, leaving the unprovable sequent ` {1 = 2} to timeout during a proof attempt” (section 5, p. 61).

Verus form. Inference: Verus branch conditions are already path assumptions in SMT. A Verus IDE could retain branch predicates in diagnostics and flag an unsatisfiable path. Equality substitution should be shown as a simplification explanation, not implemented by rewriting trusted Verus code. Use ordinary if, while, invariant, and assert; no RESOLVE Stipulate construct exists in Verus.

Evidence and limits. The contradiction example is qualitative; the paper gives no count of flagged contradictory paths. Retaining all control predicates can enlarge goals, so the paper’s relevance filter must not remove control-flow facts.

technique 4: interactive IDE feedback and derivation tracing

What it is. RESOLVE Studio combines source editing, VC generation, selectable obligations, source highlighting, prover status badges, and an interactive derivation trace from assertive code to final sequents. The paper reports that selecting a final VC “also highlights the assertion, statement, or construct that generated it within the code” (section 6.3, p. 62).

How to use it.

1. Write a contract and implementation, including loop changing, decreasing, and maintaining clauses (section 6.2, p. 62).
2. Invoke “Generate VCs” (section 6.3, p. 62).
3. Open a badge for a source construct and select one of its VCs.
4. Inspect goal and givens; invoke “prove” and read checkmark, warning, timeout, or failure status (section 6.3, p. 62).
5. For advanced debugging, step through each proof-rule application from initial assertive code to the final VC (section 6.3, p. 63).

Verus form. Inference: Verus tooling could provide a gutter marker for each generated obligation, a context-sliced view, and a derivation tree that names the Rust expression, specification clause, and invariant update. The proof remains in Verus syntax; the UI is an explanatory layer.

Evidence and limits. RESOLVE Studio had limited graduate-course use; the web IDE had years of use and positive student feedback, but the paper says additional student studies are still needed (section 9, p. 65). No controlled learning or debugging effect size is reported.

what is proved, trusted, and left open

The paper establishes an implemented VC-generation design and reports context-size reductions. Trust remains in RESOLVE’s parser/compiler, proof-rule implementation, simplifier, theory libraries, and prover backend. The study does not establish that every reported reduction preserves user comprehension, nor does it quantify proof-time changes. Inference: for a product generating agent-written verified Rust, the main threat is diagnostic opacity and wasted repair cycles rather than a new unsoundness mechanism; a context slicer must never hide assumptions from the trusted proof.

The paper notes a tradeoff in using an intermediate verification language: “Notable disadvantages however include high potential for ‘impedance mismatches’ when translating between IVLs” (section 8, p. 64). Inference: Verus should preserve Rust source provenance through any Boogie- or SMT-like lowering.

techniques for the catalog

• syntax-directed sequent VC generation — eliminate assertive code backwards, simplify sequents, and dispatch atomic obligations to a prover
• parsimonious assume with free-variable closure — retain only transitively relevant assumptions for each VC
• equality folding — substitute top-level equalities before final proving
• contradiction-aware stipulation — retain branch predicates so unreachable contradictory paths are visible
• interactive VC provenance — link each obligation to source constructs, statuses, and a derivation trace Checked 2026-10-13: audit record sun2021f; paper-study comparison complete; gate executed; experiments not rerun

Last edited: 2026-10-14