Towards Verification of Constituent Systems through Automated Proof

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

purpose and architecture

The paper presents two Symphony plugins for proving contractual properties of constituent systems (CSs) in a System of Systems: a Proof Obligation Generator (POG) and a Theorem Prover Plugin (TPP). Its abstract states, “To support verification of these obligations we have developed a proof obligation generator and theorem prover plugin for Symphony.” (abstract, p. 1) The TPP translates CML model obligations to Isabelle/HOL and attempts automated discharge; completed proof obligations are intended as evidence that a CS conforms to its contract.

CML models stateful reactive processes, types, functions, channels, operations, and CSP-style concurrent actions. Symphony’s semantic stack gives CML a UTP denotational, operational, and axiomatic foundation; the POG generates obligations and the TPP maps the CML abstract syntax tree into Isabelle/UTP definitions (§II, pp. 1–2). Isabelle’s LCF architecture provides a small trusted logical core, while auto, sledgehammer, nitpick, and a CML-specific tactic provide automation (§III–IV, pp. 2–3).

Inference: The transferable pattern for VL is a contract compiler that emits small, explicit proof obligations, then feeds each to Verus. The paper’s Isabelle/UTP semantics and CSP concurrency do not become Verus semantics automatically.

generating proof obligations

The POG categorizes goals as safe use of partial operators, safe use of functions with preconditions, type compatibility for unions, invariants and subtypes, and satisfiability of implicitly defined functions and operations (§IV, p. 3). It generates goals from a CML document for high-level properties such as internal consistency, contractual correctness, and termination. The authors describe the method: “The TPP can then be used to attempt discharge of these proof obligations, resulting in concrete proof objects for the properties.” (abstract, p. 1)

The division example shows the repair loop. For division(x,y) == x / y, the POG initially generates forall x:int, y:int & (y <> 0), which is unsatisfiable because arbitrary y may be zero (§IV, p. 3). Adding the precondition pre y <> 0 makes the operation obligation dischargeable. The call divby2(x) == division(x,2) then creates a separate precondition obligation requiring pre_division(x,2) at every call site (§IV, pp. 3–4). The workflow is therefore: generate an obligation; inspect a failed formula; strengthen the operation precondition or add a guard; regenerate; discharge the revised formula; and check every caller obligation.

Inference: In Verus, use requires for the divisor condition, ensures for the result, and call-site proof obligations generated by Verus when invoking the function. A failed call obligation is repaired by proving the required precondition in the caller, not by weakening the callee contract. Verus spec fn and proof functions can express mathematical division conditions, while executable division still needs an appropriate Rust type and runtime behavior.

translation and automated discharge

The TPP deep-embeds CML: it gives explicit Isabelle semantics to process operators, translates the CML AST and POs into Isabelle theory files, and invokes tactics. The paper says, “These theory files can then be submitted to Isabelle for discharging through various automated proof tactics such as auto and sledgehammer, or the cml tac tactic that maps a CML formula onto a HOL formula.” (§IV, p. 4) Users may select individual POs in a fully automated mode, or write model-specific conjectures directly in Isabelle for manual proofs.

The tool offers Quick check and Proof Session modes. Quick check rapidly lists current POs and links them to model elements so failed goals can guide guards and preconditions. Proof Session snapshots a timestamped read-only model, regenerates POs and theories, discharges selected goals, and stores the results with that snapshot (§IV, pp. 4–5). The snapshot matters because proofs are valid only for the model version from which the POs were generated.

Inference: A Verus integration should generate a stable proof target from a versioned Rust module, retain the exact source and dependency versions, and rerun obligations after edits. Verus checks the resulting Rust contracts directly; an external translator would add a trusted semantic boundary comparable to the CML-to-Isabelle translation.

constituent-system example

The paper models a railway Dwarf Signal CS with a DwarfType state record, a ProperState subtype (dark, stop, warning, drive), invariants such as NeverShowAll, MaxOneLampChange, ForbidStopToDrive, DarkOnlyToStop, and DarkOnlyFromStop, and operations Init, SetNewProperState, TurnOn, and TurnOff (§V, pp. 5–6). Init sets all fields and has a postcondition requiring the resulting fields to equal the stop state and empty turn-on/turn-off sets. The POG emits subtype-invariant obligations and a postcondition obligation for that assignment.

The authors report that discharging all POs would provide a model “verified to be both internally consistent and, through encoding the safety properties which must be met by the signal, safe with respect to the requirements placed on that contract.” (§V, p. 6) However, the same section reports that several state-dependent POs were not discharged; possible causes were incorrect VDM-derived expressions or immature proof tactics (§V, p. 6). The POG also does not handle CML actions that dictate event ordering, so those actions are omitted from the example (§V, p. 6).

Inference: In Verus, encode the state record as a Rust struct with a representation invariant proved by a predicate, and prove each operation’s ensures preserves that predicate. Concurrent event ordering requires a Verus state-machine or other explicit transition model; a sequential struct invariant alone is insufficient.

evidence, trust, and limits

The paper provides architecture, proof-goal categories, formulas, a worked railway model, and screenshots of discharged and failed obligations. It reports no benchmark denominator, timing distribution, success percentage, or defect-detection rate. Its concrete evidence is a prototype and a small illustrative CS model. The authors propose future Hoare or weakest-precondition calculi for richer process/state obligations, SoS-level interface composition, refinement provisos, and more Isabelle tactics (§VI, pp. 6–7).

What is proved is conditional: each discharged PO is checked by Isabelle’s kernel against the generated CML/UTP theory. What remains trusted includes the CML specification, POG translation, CML/UTP semantic embedding, Isabelle implementation and libraries, and the model’s contract itself. Inference: For agent-written verified Rust, the threat is specification drift and incomplete obligation generation. A green Verus proof can establish only the emitted contract; omitted concurrency, external calls, hardware, or caller assumptions remain unchecked. Existing POG/TPP work means VL should not redo generic precondition, subtype, and postcondition obligation enumeration without adding Rust/Verus-specific coverage or evidence.

techniques for the catalog

• proof-obligation generation — enumerate partial-operator, precondition, subtype, invariant, postcondition, and satisfiability goals from a model
• contract repair by failed obligations — use an unsatisfied PO to add a guard or strengthen a precondition, then regenerate caller obligations
• semantic AST translation — deep-embed the model language and translate its AST and obligations into a theorem prover’s logic
• automated tactic discharge — invoke trusted-kernel tactics such as auto, sledgehammer, or a domain-specific tactic on generated theories
• versioned proof sessions — snapshot the model, regenerate obligations, discharge them, and retain proofs with the exact source version
• constituent invariant verification — prove each operation’s postcondition and subtype/invariant obligations for a stateful system model

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15