Appendix B — Models-bridge patterns

Appendix B - 11. Formal invariant verification (temporal form → model checking)

The Structure of Formal invariant verification (temporal form → model checking) — its shape at a glance:

Each invariant declares a temporal operator. A router reads the operator and picks the checker its shape demands; a match lint asserts the routed checker matches the operator, so a mis-declared invariant is a build error, not a silent gap.

flowchart TD
  Inv[Invariant + temporal form] --> Op{Operator?}
  Op -->|always P| Safety[State-space search]
  Op -->|P leads-to Q| Live[Temporal model checker]
  Safety --> Lint{{Match lint}}
  Live --> Lint

Accessible description: an invariant carries a temporal operator that a decision routes — a safety "always" operator to a state-space search, a liveness "leads-to" operator to a temporal model checker. A match lint checks the routed checker against the operator and fails on a mismatch.

Projected from the catalogue entry system-models / Formal invariant verification (temporal form → model checking).

On this page: Intent · Motivation · Applicability · Structure · Sample Code · Consequences · Example use within DocAble · Related Patterns

Intent

Intent — Give every model invariant a temporal form: a temporal-logic operator saying whether it is safety ([]P, always holds) or liveness (P ~> Q, eventually leads to), and make that form the routing input: it derives which exhaustive checker verifies the invariant. An invariant is then proven by the method its shape demands, a state-space model-check rather than a sampled test, and it cannot be silently mis-verified (our instance: temporal-logic operators on the cross-service state model, checked by a model checker plus a bounded-BFS "simworld").

Motivation

Some invariants are about a single reachable state: "a job is never both leased and free." Others are about interleavings over time: "a preempted job eventually re-runs." Stated in prose, or pinned by one example test, either kind can be believed true while a rare interleaving violates it: a property test samples the input space and sails past the one adversarial schedule; a distributed race has failure traces no hand-picked example hits. Worse, when the same invariant is restated in three places (prose, a runtime assertion, a formal spec) with nothing tying them, they drift; and a mis-declared liveness invariant gets routed to a safety runtime that structurally cannot see its violation, with zero signal.

Applicability

Structure

The Structure diagram appears at the top of this page.

Sample Code

The temporal form is a required field that derives the checker. A router maps the operator to an exhaustive checker, and a match lint fails when the two disagree — so "a liveness property checked by a safety runtime" is impossible rather than silent.

import sys

def route(temporal_form: str) -> str:
    """The operator shape derives the checker. Required field, consumed here."""
    if "~>" in temporal_form:            # leads-to => liveness
        return "temporal-model-checker"
    if temporal_form.startswith("[]"):   # always => safety
        return "state-space-search"
    raise ValueError(f"unrecognized temporal form: {temporal_form!r}")

def match_lint(invariants: list[dict]) -> list[str]:
    """The routed checker must match the operator (no mis-declared invariant)."""
    findings = []
    for inv in invariants:
        want = route(inv["temporal_form"])
        if inv["checker"] != want:
            findings.append(f"{inv['name']}: routed to '{inv['checker']}', form needs '{want}'")
    return findings

if __name__ == "__main__":
    # `load_invariants` returns each invariant's name, temporal_form, and routed checker.
    findings = match_lint(load_invariants())
    for f in findings:
        print(f"MIS-ROUTED: {f}")
    sys.exit(1 if findings else 0)

Consequences

Example use within DocAble

Contents
⇐ Beginning of this partNext part ⇒Next chapter ›⇤ BeginningEnd ⇥Index
© James C. Davis, 2026–present