Mostly Automated Proof Repair for Verified Libraries

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

problem and result

The paper repairs proofs of imperative OCaml library functions after local changes to their code while the specification stays fixed: “In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged” (Abstract, p. 1). The input is an old OCaml program p, its separation-logic specification, its CFML/Coq proof P, and an unverified new program p′ believed to satisfy the same specification; the output is a proof P′ (Introduction, p. 3). The motivating refactoring replaces a for-loop over array indices with Array.iter; the paper says finding the new invariant “is a daunting task for general-purpose automated program verifiers”, while the old proof contains useful information (Introduction, p. 2). The paper states: “The goal of this work is to turn this intuition into a practical proof repair algorithm for libraries” (Introduction, p. 2). The authors build Sisyphus, combining proof-skeleton generation, dynamic program alignment, enumerative invariant synthesis, and proof-driven testing (Fig. 4, p. 7).

technique: reconstruct a proof skeleton

Use this when the new program has the same CFML specification but its proof script is missing. First encode loops as applications of higher-order combinators, so loop-invariant inference becomes invariant inference for higher-order function applications (Sec. 3.1, p. 12). Traverse the new program syntax and map values, conditionals, pattern matches, lets, and applications to CFML tactics: xval., xif., xmatch., xletval v., and xapp. (Figs. 9–10, p. 12). For a higher-order application emit xapp s (fun q ⇒ □)., leaving an invariant hole. Use the function dictionary E to retrieve function specifications and add their side conditions to the list of residual obligations; xval emits the heap entailment P ⊢ Q v (Sec. 3.1, p. 12). Residual obligations go to a user-provided solver tactic (user_solve), and each goal it fails on becomes an admit for the user (Sec. 2.2, p. 8). The paper’s example maps function applications to xapp, array allocation to xalloc, empty-array creation to xvalemptyarr, and branching to a case analysis in the proof (Sec. 2.2.1, p. 8). The skeleton mirrors the program but does not guess the invariant.

Inference: in Verus, write the new Rust function and its requires/ensures, then use a while loop with an explicit invariant clause or a proof-oriented higher-order wrapper. Verus has no CFML tactics or Coq proof script; the structural translation is a design analogy, not a paper result. The unchanged part is the executable algorithm and contract; the changed part is the Rust proof syntax and ownership facts.

technique: dynamic program alignment

Use this when old and new implementations compute the same logical result through different intermediate computations. For each randomly generated input, execute p and p′ and record the program state (heap and stack) at every program point. Normalize aggregate values through canonical projections (for example, arrays and sequences both become lists; users can supply their own projections). Score two states by summing the sizes of normalized values present in both; the algorithm maps each new program point to the highest-scoring old point, so many new points can map to one old point but not vice versa (Algorithm 3.1 and Sec. 3.2, p. 13). The paper says: “We run p and p′ on the same randomly generated input, collecting traces of their execution and recording the values of all program variables at each statement” (Introduction, p. 3). In the to_array example, the call to iteri aligns with the call to fold_left “as both produce arrays with the same payload, even though they do so in different directions” (Sec. 2.2.2, p. 10).

Inference: a Verus implementation could instrument executable Rust tests, normalize arrays or sequence abstractions, and use the resulting map to select old lemmas or invariant templates. This is heuristic evidence, not a proof; Verus must still prove the selected invariant for all inputs. A Rust analogue must also account for ownership and borrowing states, which the paper does not address.

technique: template and enumerative invariant synthesis

For every invariant hole, construct a template from the heaplets in the symbolic state immediately before the new program point: keep each heaplet’s points-to predicate and replace its arguments with holes; add an equality hole v = _ for each invariant parameter (Algorithm 3.2, p. 14; e.g. template (8), p. 14). Retrieve the invariant at the aligned old point, make expression sketches by replacing subexpressions with holes, collect constants and function symbols from the old proof, and add logical variables from the specification; enumerate fillings of the sketches into the template (Sec. 3.3 and Algorithm 3.2, p. 14). In the running example, the old iteri invariant yields the sketch (_ ++ drop _ _) and the simplified template fun (acc: int) (t: list A) => a ↦→ Array (_ ++ drop _ _) (Sec. 2.2.2, p. 10). Whenever possible, the heap and pure parts of candidates are tested independently rather than as their product (Sec. 5, p. 20).

Inference: use a Verus invariant containing the corresponding sequence/array relation, and make candidate expressions from existing spec fns, constants, and ghost state. Verus syntax and ownership conditions are different; the paper’s separation conjunction and CFML predicates do not carry over directly. The useful transferable idea is search-space restriction from an aligned previous proof.

technique: proof-driven invariant testing

Use this before expensive proof checking when candidate invariants are numerous. Instantiate the Coq proof term of a higher-order function’s specification with concrete arguments and the candidate invariant, and reduce it to head-normal form; the types of its non-reducible subterms contain the property applied to concrete values (Sec. 4.1, p. 15). Extract an OCaml test from the reduced term: unlike vanilla extraction, which erases proof terms, the new rules emit an assertion wherever a subterm’s type can be reflected into an executable check (Sec. 4.2, p. 16). For CFML, reflection maps separation-logic heap predicates to OCaml functions over their contents, and the xapp rule inserts an assertion of the precondition before the call; postconditions are not converted (Sec. 4.3, p. 17). Algorithm 4.1 runs the new program on a random input up to the higher-order call, instantiates and reduces the proof term, extracts a test, and runs it from the captured state (Sec. 4.3, pp. 17–18). The concrete fold_left test in Fig. 7 asserts the invariant before the first step and after each accumulator update; the incorrect candidate, which says all array elements are equal, fails when the array becomes [3; 2; 3] (Sec. 2.2.3, p. 11). The paper says: “If δ raises an exception during its execution, then I is invalidated and can be pruned away” (Sec. 4.3, p. 18).

Inference: Verus proof code is erased and is not a Coq term with this reduction behavior, so this exact extraction method does not carry over. A Verus analogue would generate runtime tests from candidate ghost/spec expressions, then use those tests only for pruning before ordinary Verus verification. The tests cannot establish universal validity.

evidence, limits, and trust

The paper says Sisyphus is “19k lines of OCaml”; its component table totals 18,800 lines, including 7,600 for modified Coq reduction and 1,600 for reflection and extraction for CFML (Sec. 5, p. 18). Obligations are dispatched by a domain-specific solver of about 700 lines of Ltac; an initial implementation used Z3, which was “taking several minutes on even simple goals” (Sec. 5, p. 18). The benchmark has 14 evolved programs, 10 mined from popular OCaml libraries; the changes are in iteration order, intermediate data structures, mutable-to-pure, and pure-to-mutable, over arrays, lazy sequences, mutable singly-linked lists, stacks, queues, and trees (Sec. 5, p. 18). The authors report: “Sisyphus was able to automatically construct new proofs for all programs in our benchmarks: all synthesised invariants were valid” (Sec. 5, p. 19). Another author proved the admitted obligations manually; Table 2 reports 0–3 admits among 1–7 obligations per program, and “all obligations took fewer than 20 minutes to dispatch” (Sec. 5, p. 19). Most repairs ran in under two minutes on a 3.5 GHz Apple M2 MacBook Air with 8 GB RAM (Sec. 5, p. 19); array_foldi took 504 seconds and sll_partition 443 seconds, mostly spent extracting tests (Table 3 and Sec. 5, p. 20). Candidate totals range from 22 to 6.2×10^11; generation is lazy, so counts stop when Sisyphus finds a suitable invariant or gives up (Table 3 and Sec. 5, p. 20).

The paper’s failure assumption is explicit: “An important assumption of Sisyphus’s repair process is that components of the old proof, such as the lemmas and functions that it uses, will be sufficient to prove the new program correct” (Sec. 5, p. 20). For array_partition, the new proof needed a lemma about repeated filters absent from the old proof; if the new program needs a function absent from the old proof, no candidate in the search space can pass proof-driven testing and repair fails entirely; a batching to_array variant fails because its invariants need list-of-lists flattening (Sec. 5, p. 20). Inference: the repaired proof is checked by Coq, so alignment, normalization, and extracted tests affect only which invariants are found, not soundness; the unchanged specification and the Coq/CFML framework remain trusted. Inference: for a product generating Verus Rust, this is a medium threat and opportunity: proof maintenance can be cheaper when refactorings preserve contracts, but heuristic alignment and candidate tests cannot replace universal checking, and changed APIs or missing lemmas still require new human proof work. The product should retain generated proof artifacts and measure residual obligations rather than claim full automation.

techniques for the catalog

• proof-skeleton reconstruction — map new syntax to proof actions and leave higher-order invariants as explicit holes
• dynamic program alignment — execute old and new versions on shared random inputs and map states by normalized-value similarity
• template and enumerative invariant synthesis — derive heap-shaped templates and enumerate expressions mined from the old proof
• proof-driven invariant testing — reduce higher-order proof terms into executable assertions that prune invalid candidates Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Note that alignment is a many-to-one correspondence: many new program points can map to one old program point (but not vice versa).”): what I checked: every quotation, number, section, page, figure, table and algorithm reference, and each technique step against the paper text, and the tag and DOI link; what I changed: corrected the goal-sentence page (2, not 3), the alignment and Algorithm 3.1 pages, heap/pure separation (testing, not generation), the data structures (mutable singly-linked lists, not lists), the 19k vs 18,800 lines figure, the lazy-count condition (“or gives up”), added the abstract quote and missing technique details (user_solve/admits, extraction and reflection, xapp precondition only), and replaced the trust list with an “Inference:” that Coq checks the repaired proof; what I did not check: the Verus inferences, the artefact, and two-column layout beyond the text dump.

Last edited: 2026-10-17