Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, table count, page and section reference, quotation, the steps of techniques 1 to 5, the R1 to R10 list and the arithmetic; changed four slips (audit classes taken from the separate declaration map in 7.1, seam-definition rule widened beyond the paper, v0.10 called the skeleton, clean build claimed throughout) and softened one unchecked claim about Mathlib names; Verus forms are labelled inference and unchanged, with assume_specification not confirmed in the Verus reference.

source: Woodcock, Leite, Sampaio, Wei, arXiv:2608.18822v1 (19 Aug 2026), 15 pages, no appendix; submitted to Formal Methods for Autonomous Systems 2026; artefact at Zenodo doi 10.5281/zenodo.21981425 (not read)

relation to earlier notes: the tool used here, CAPRI, has its own paper by the same authors, studied in capri_20261013.md in the walkthrough directory. That study covers the acceptance rule Build ∧ Conforms, the contract file format, the outcome labels, the classifier controls and the 180-run experiment. This paper is the field report: one development that drifted before the tool existed, how the drift was measured, and how the development was rebuilt under contracts. Only what this paper adds is written out below.

the case in five sentences

An Isabelle/HOL model of a controller for two cascaded water tanks was started as nine theory files with the main theorem statements written and ten proofs left open (§3.2, p.4; §4, p.4). ChatGPT proposed proofs and lemmas; each candidate was built in a throwaway copy; the developer picked which state to continue from; nothing protected the statements or definitions (§4, pp.5-6). After 59 substantive states the development had 16 theories and built with no sorry, oops, added axiomatization or oracle (§1, p.2; §4, p.6). A later comparison with the first outline found that 16 of its 100 named declarations had changed in content, and that the headline theorem now assumed three of the four requirements it concluded (§6, p.7; §6.1, pp.7-8). The authors then rebuilt the ten proofs inside the original nine files under per-task edit contracts, and left one gap open under a name (§7, pp.9-10; §8, p.11).

The opening sentence of the abstract is the thesis: “Large language models can propose proofs for interactive theorem provers, but a successful build does not show the surrounding verification task was preserved.” (Abstract, p.1)

Three definitions the paper introduces and the rest of this study uses (§1, p.2):

• “The theory frame is the set of statements, definitions, assumptions, imports, file structure, and public claims that delimit the authorised proof task.”
• “Theory drift is an accumulation of individually accepted edits that changes that task without an explicit change of intent.”
• “A semantic seam is a boundary between separately formalised layers that needs an explicit bridge before their meanings can be treated as connected.”

Everything said about Verus below is this study’s inference from an Isabelle paper.

proved, measured, trusted

• proved in Isabelle2025-2: the ten scoped obligations R1 to R10, in a nine-theory session with zero oops, sorry, axiomatizations and oracles (Table 4, p.11)
• not proved: that executions of the modelled plant, sampler and controller satisfy the trace predicate the final theorem assumes. “The open question sits one layer earlier: the release does not yet show that every coherent trace generated by repeated plant, sampling, and controller execution satisfies every clause of is_closed_loop_trace.” (§8, p.11)
• measured by hand with machine help: the 16-of-100 audit. “The 16/100 result therefore combines mechanical comparison with manual semantic classification: the archived map and rationales are inspectable, but the classifications remain interpretive and were not independently adjudicated.” (§6, p.7)
• trusted: “The contract checker is trusted tooling and has not itself been verified in Isabelle.” (§9, p.12); also the developer’s judgement on every widened contract, and the replay, which was done by a co-author and is called internal (§8, p.11)
• models: ChatGPT 5.0 in the drifting phase, without stable identifiers for every interaction; GPT-5.2 (gpt-5.2-2025-12-11) at high reasoning effort inside CAPRI, each request independent (AI Usage, pp.12-13)
• not a comparison: “The study follows one evolving double-tank repository and makes no comparison between alternative CAPRI repair configurations.” (§1, p.2)

technique 1: a declaration-level drift audit against the first outline

what it is: a census of every named declaration in the earliest version of a development, each compared with what it became.

when to use: after any stretch of model-assisted proof work in which statements and definitions were editable, before making claims about what was proved.

how it is done (§6, p.7; §7.1, p.9):

1. fix the universe: the named declarations of the earliest frame, here 100; names added later (here 295) are recorded separately and are not part of the count
2. generate inventories and a candidate correspondence between old and new declarations by machine
3. a person inspects every non-identical pair and every rename, split or merge, and records a relationship class and a reason
4. the test for unchanged: the formal statement or definition body is the same, ignoring presentation-only edits
5. the classes the paper lists for its declaration map (§7.1, p.9; the paper does not say these are the classes of the 16/100 audit, and it speaks of each significant original declaration): “We mapped each significant original declaration to its v0.23 counterpart and classified it as preserved, renamed, specialised, generalised, split, merged, reformulated, superseded, missing, rejected, or added.” (§7.1, p.9)
6. group the changed ones by their effect on the engineering argument, not by syntax (Table 2, p.7)
7. do not count every change as a defect: a seam needs a definition eventually, and some proofs needed explicit guards or frame conditions (§6, p.7)
8. separately, trace each top-level requirement from its physical motivation through definition, assumptions, theorems, translation layers and run-time monitor, so a change shows where it touches the public interface (§7.1, p.9)

what it found (Table 2, p.7), 16 changed of 100, 84 identical:

• 4 semantic instantiation or refactoring: the three seams received definitions, and the availability requirement was refactored through a parametrized version
• 4 plant and assumptions: plant evolution, guarded capacity, one-cycle and finite-iteration preservation; sounder argument, narrower admitted plant
• 6 safety domain and boundary: safe_at, the safety requirement, the overflow monitor and its soundness and coverage results; strict < became ≤ and the requirement was restricted to non-negative time
• 2 end-to-end interface: three requirements moved into the premises of the public claim The four counts sum to 16. Of the ten obligations left open at the start: “Among the ten original unfinished obligations, six were proved unchanged and three only after reformulation.” (§6, p.7); the tenth, the unconditional end-to-end theorem, stayed open.

Verus form. Inference: the universe is every spec fn, every proof fn signature, every executable function’s requires and ensures, and every type definition in the first version of the crate that carried the intended contracts. The unchanged test is textual equality of the signature and clauses for functions and of the body for spec fns after formatting. Step 2 is a script over two source trees; step 3 stays manual. Inference: for VL this audit is the after-the-fact counterpart of freezing contracts, and it is the only one of the two that can be run on work already done.

evidence: one development, one audit, by the people who wrote the development.

where it fails: it needs an earliest frame worth trusting. Here the outline was written before the proofs (§4, p.4); a project whose contracts were first written by the same agent that later proved them has no such reference.

technique 2: five shapes of drift to search for

what it is: the paper’s concrete catalogue of how a development that still builds can stop meaning what it was meant to. The grouping into five is this study’s; each item is the paper’s.

1. conclusion moved into the assumptions under an unchanged name. The intended theorem assumed admissible parameters and a closed-loop trace and concluded safety, settling, stable tracking and availability; the drifted one assumed admissible parameters and the last three, and concluded all four (extract, §6.1, p.8). The result was then exported as double_tank_end_to_end_assurance. “This is a characteristic form of drift: the theorem name and its architectural position preserve the appearance of the first claim even though the logical burden has quietly moved into the assumptions.” (§6.1, p.8)
2. a boundary relaxed by one symbol. safe_at changed from level < capacity to level ≤ capacity for both tanks, and the monitor now reports OK at exactly full (§6.1, pp.7-8). “The revised definitions and monitor theorems were internally consistent, yet they certified a weaker policy than the first outline.” (§6.1, p.7)
3. a domain narrowed: the safety requirement restricted to non-negative time; the admitted plant and parameter domain restricted (Table 2, p.7)
4. a placeholder predicate defined so that the theorem about it becomes easy. is_closed_loop_trace was defined by pointwise reachability, though separately reachable observations need not form one execution (§6.1, p.8). “A trace theorem can then become easy to prove if the trace predicate already includes the desired property or admits observations independently of their temporal relationship.” (§6.1, p.8)
5. architectural bypass: with added abstraction layers, a layer may replace the source semantics instead of representing it, a direct theorem may skip the satisfaction condition, a translation may change a requirement’s meaning, a conditional result may be exported under an unconditional name (§6.2, pp.8-9)

the invariants the authors fixed against item 5 (§6.2, p.9): layers preserve the source semantics; transported results depend on a proved satisfaction condition; each of the four requirements has a traceable source-to-target mapping; public all-requirements claims expose any premise still unproved.

Verus form. Inference, item by item:

• item 1 is an ensures conjunct that reappears in requires. A script can flag it: any expression present in both clauses of one function, or newly present in requires and formerly only in ensures. In Verus the move breaks callers that cannot establish the new precondition, but a top-level function has no verified caller, so for the function that carries the product’s headline guarantee nothing breaks
• item 2 is < against <= in a spec fn or clause; a diff restricted to comparison operators in protected regions finds it
• item 3 is an added requires conjunct or a parameter type narrowed, for example int to nat
• item 4 is a spec fn used in a requires whose body is edited until it contains the ensures. The check is to read the body of every predicate a headline theorem assumes and ask whether the conclusion is one of its conjuncts
• item 5 has a direct counterpart when executable code is connected to a model through several spec fn views: a proof about the top view that never goes through the function that links code to view proves nothing about the code

evidence: these are the 16 audited changes; no frequency beyond this development.

technique 3: escalate authority by named contract, never by a wider patch

what it is: the rule for what happens when a proof cannot be finished without changing something outside the proof. The base mechanism (edit contract, Build ∧ Conforms) is in the CAPRI study; this is the escalation discipline around it.

how it is done (§5, p.6; §7.1, pp.9-10):

1. a proof-only contract freezes the theorem statement, assumptions, locale context, definitions, imports, file set, all text outside the proof, the Isabelle version and the build command (§7.1, p.9)
2. the checker is run before the build and again after it. “The first check kept obviously unauthorised candidates from consuming prover time; the second caught changes introduced by patch application or an iterative tool outside the displayed proof proposal.” (§7.1, p.9)
3. three end states: accepted repair (both pass); safe failure (proof fails, frame intact); false success (Isabelle accepts, checker finds an unauthorised change) (§7.1, p.9)
4. when the proof cannot be done under that authority: “When an obligation could not be solved honestly under that authority, the workflow did not silently widen the patch; it required a new contract for a statement change, semantic extension, architectural change, or conservative new theory, and that broader contract had to name the permitted change and retain the existing obligation in the record.” (§7.1, p.9)
5. chain the baselines: “Each accepted state became the protected baseline for the next task, so the authority to change the development expanded only through an explicit contract.” (§7.1, p.9)
6. order the tasks by semantic dependency, so the last theorem has to use the earlier results (§7.1, p.10): plant semantics at zero duration (R1), non-negative levels (R2), capacity under guard (R3), sampling period (R4), tolerance budget (R5), safety transfer (R6), tracking transfer (R7), one-cycle preservation (R8), iteration (R9), the four requirements (R10) (Table 3, p.10)
7. keep rejected candidates with their diagnostics. For R10: “Two candidates used unavailable facts or methods (diff_nonneg, sub_nonneg, and nlinarith) and left the conformance argument incomplete.” (§7.1, p.10); a third passed both checks

the limit the paper puts on its own checker: “Thus Conforms detects unauthorised structural edits but cannot judge semantic equivalence inside an authorised region; a permitted rename, scope change, or replacement definition still requires explicit wider authority and substantive semantic review.” (§5, p.6). The comparison is by repository, file set and source region, not by syntax tree (§5, p.6).

the one control reported here: “A control where the target theorem was weakened to a trivial statement demonstrated the distinction: Isabelle accepted the altered theory, while CAPRI rejected the delta.” (§5, p.6)

Verus form. Inference: a proof-only contract for a Verus function has to say more than “the body”, because in an executable function the body is also the program. Proof-only means: proof { } blocks, assert statements, invariant and decreases clauses of loops, ghost variables, and bodies of proof fns may change; the signature, requires, ensures, executable statements, every spec fn body, use lines, other files and the verifier’s command line may not. The forbidden list is assume, admit(), #[verifier::external_body] and assume_specification. Inference: the escalation ladder then has natural rungs: add a new proof fn in a named region; change an executable statement; change a spec fn; change a requires or ensures. Each rung is a different contract with a human decision, and the last two are the ones the audit of technique 1 would later count as drift if taken silently. Inference: the paper’s remark on porting holds for Verus as it does for the provers it names: “A Lean or Coq port would need prover-specific adapters for declaration and proof-region location and for dependency/build metadata.” (§2, p.3)

evidence: ten obligations discharged, every accepted change conforming to its contract (§8, p.11). The paper gives no count of candidates generated, rejected or falsely successful during R1 to R10; R10’s three candidates are the only ones described.

where it fails: see the R10 point under disagreements.

technique 4: keep a seam visible, and give an unclosed gap a name and a statement

what it is: two halves of one habit. At the start, a layer whose meaning is not yet chosen is left as a named placeholder instead of being filled with something convenient. At the end, a connection not yet proved is written as its own theorem statement with an identifier, outside the accepted release.

how it is done:

1. in the first outline, three placeholders stood for meanings to be supplied later: solves_tank_ode for the continuous dynamics, state_duration for the measure of time in a state, is_closed_loop_trace for the relation between traces and repeated execution (§3.2, p.4)
2. the stated risk of step 1: “It also created a risk: when a seam was later defined, its definition had to capture the intended semantics rather than make the target theorem true by construction.” (§3.2, p.4)
3. when a seam definition risks making the theorem true by construction, treat it as a semantic change needing recorded provenance and a successor obligation linking it to the operational model; the paper applies this to defining is_closed_loop_trace by pointwise reachability, and calls the concrete meanings given to solves_tank_ode and state_duration necessary progress (§6.1, p.8)
4. at the end, state the missing link as a theorem to be proved from a new baseline; here DT-R011, with assumptions admissible parameters and an operational closed-loop trace and conclusion is_closed_loop_trace (§8, p.11)
5. the accepted release stays immutable; the successor starts from a named new baseline (§8, p.11)

the paper’s summary of the habit: “An unresolved semantic bridge has been given a stable identifier and an explicit statement, rather than being folded into an assumption or hidden behind an overbroad theorem name.” (§8, p.11)

Verus form. Inference: the gap named DT-R011 is the gap between a proof about a model and a proof about the code. In Verus it is closed when the executable function’s ensures states the property and the verifier checks the body against it; it is open when the property is proved only as a proof fn over spec fns that describe what the code is supposed to do. A VL deliverable should say for each headline property which of the two it is. Inference: writing the open link as a proof fn with a body of admit() would put the name in the code but breaks the no-admissions rule of the release, so the paper’s choice of keeping the statement outside the accepted build is the one to copy.

evidence: none beyond the case.

technique 5: rescue from two frozen sources

what it is: recovering a drifted development without discarding the proofs found along the way.

how it is done (§7.1, p.9):

1. freeze the original frame; it supplies the task: definitions, requirements, theorem statements, seams
2. freeze the drifted but building repository; it supplies proof knowledge: lemmas, reusable proofs, and the failed approaches that exposed hidden assumptions
3. add provenance records, the declaration correspondence, architectural constraints, contracts, public-interface checks, manifests and hashes
4. rebuild in a separate source tree, inside the original file structure, taking mathematics from the second source and statements from the first
5. where the chain of meaning is incomplete, name the missing link as a successor obligation; do not add it to the assumptions of the theorem under repair (§1, p.2)

Verus form. Inference: nothing in this is specific to a prover; with Verus the second source is the drifted crate’s proof fns and loop invariants, and the first is the original signatures and spec fns.

evidence: the reconstruction finished within the nine-theory structure; the 16-theory version is kept as a separate baseline (§9, p.12).

three smaller practices from the drifting phase

• outline first: fix vocabulary and headline statements in a skeleton with the hard proofs marked unfinished, and order the work by semantic dependency (§4, pp.4-5). At v0.10 the nine theories were 953 lines with 40 definitions, 28 lemmas, 19 theorems and ten oops (Table 1, p.5)
• keep every state: after removing byte-identical and packaging-only copies, 59 substantive states were archived, 23 stable and 36 broken; the failures exposed unavailable facts, hidden analytic side conditions, weak induction hypotheses, missing frame conditions, and mismatches between the physical argument and the formal goal (§4, p.6)
• a check that generic machinery is generic: the added institution layer was instantiated with a second, independent model, a thermostat (§3.2, p.4)

Inference: keeping every state is the practice that made the audit possible at all; without archived states the 16 changes could have been counted but not explained.

where the paper disagrees with itself

• Inference: R10’s premise carries part of its conclusion. The final theorem assumes is_closed_loop_trace, and the paper says the four requirements are derived from that predicate’s explicit clauses, “including strict-safety and uniform-tracking clauses” (§8, p.11). The paper calls this trace contract non-circular (Table 3, p.10) and elsewhere warns against a trace predicate that already includes the desired property (§6.1, p.8). The statement of R10 has the same shape as the originally intended theorem, so no contract on the statement is violated; the weight sits in the predicate’s definition and in DT-R011. The paper is open that DT-R011 is unproved, but the abstract’s sentence that the reconstruction discharged all ten scoped obligations is true only with that reading of “scoped”.
• Inference: the last and most important step did not run under a proof-only contract. The R9-to-R10 change was confined to four files, among them the requirements theory (§7.1, p.10), and Figure 2 (p.6) describes its contract as schematic and not verbatim. What the developer authorised inside those four files is not shown.
• Table 1 (p.5) gives 40 definitions, 28 lemmas and 19 theorems for v0.10, which is 87; the audit’s universe is 100 named declarations of the earliest frame (§6, p.7). The paper does not say what the other declarations are or whether the two versions differ.
• §8 (p.11) cites ten DT-R010 self-tests and six static Action 8 controls reproduced in the replay; neither is described anywhere in the paper. Only the one weakened-theorem control of §5 is.
• Inference, unchecked: nlinarith looks like a Lean Mathlib tactic name, which would suggest the model sometimes answered in another prover’s vocabulary; I did not check Isabelle’s library for these names. The paper reports the names as unavailable facts or methods and draws no conclusion.
• the arithmetic that can be checked holds: 23 + 36 = 59; 84 + 16 = 100; 4 + 4 + 6 + 2 = 16; 6 + 3 + 1 = 10.

reusable as it stands

• the eleven relationship classes for a declaration map
• the four architectural invariants
• the escalation rule of technique 3, step 4
• the three definitions quoted at the top; “theory drift” and “semantic seam” name things VL will need words for

threat to VL

Inference, all of it. As a competitor, none: one small Isabelle model of a control system, no code verified, a tool specific to Isabelle. As evidence about the product’s central risk, strong and specific: an unconstrained model-assisted proof effort by formal-methods experts changed 16% of the original declarations and ended with a headline theorem that assumed three quarters of what it claimed, while Isabelle accepted the final 16-theory development. A product that sells agent-written verified Rust has to be able to show this did not happen to it, which means frozen contracts checked outside the verifier, and a drift audit of the kind in technique 1 for anything produced before the freeze. The paper also shows the residue such controls leave: even the governed reconstruction ended with the hardest link unproved and the final step done under widened authority whose content the reader cannot see.

techniques for the catalog

• declaration-level drift audit — take every named declaration of the earliest version, map it to its current form by machine, classify each non-identical one by hand, and report changed over total
• eleven-class correspondence map — label each old declaration preserved, renamed, specialised, generalised, split, merged, reformulated, superseded, missing, rejected or added
• conclusion-in-premises check — flag a theorem whose assumptions contain conjuncts of its own conclusion, especially under a name that suggests an unconditional result
• boundary-operator diff — treat any change between strict and non-strict comparison in a safety definition as a change of requirement
• seam-definition review — when a placeholder predicate that a headline theorem assumes receives a definition, check that the definition does not contain the theorem’s conclusion
• requirement traceability chain — link each top-level requirement from motivation through definition, assumptions, theorems, translations and monitor
• architectural invariants for layered proofs — require that added abstraction layers preserve source semantics, that transported results rest on a proved satisfaction condition, and that public claims expose unproved premises
• double contract check — run the conformance check before the prover to save prover time and again after it to catch edits made during patching or iteration
• named authority escalation — when a proof needs a change outside its region, issue a new contract that names the change and keeps the old obligation on record
• chained baselines in dependency order — make each accepted state the protected baseline of the next task and order tasks so the final theorem must use the earlier ones
• visible seam — leave an undecided layer as a named placeholder in the outline instead of filling it with a convenient definition
• named successor obligation — write an unproved link as an explicit theorem statement with an identifier, outside the accepted release
• two-source rescue — rebuild a drifted development from the original statements plus the drifted version’s proofs, in a separate tree
• archive of broken states — keep failed candidates and diagnostics, since they explain why later statements and assumptions changed
• second-instance generality check — instantiate generic proof machinery with an unrelated model to show it was not specialised to the first

Last edited: 2026-10-13