Saltar al contenido principal

ADR 017 — Formal specifications for critical state machines (TLA+/Apalache)

  • Status: Accepted (2026-08-03, scoped) via the ARP review — adopted as a scoped constraint: replay-convergence proof obligations apply to the ARP event-spine saga runner and any newly modeled transition table (order states, approval states); no broader formal-spec mandate. Supersedes the Proposed (2026-06-19) E1/Wave-1 gating. See alphaswarm_internal docs/architecture/agent-first-research-platform/02-context-map-and-ownership.md §6 (binding disposition table) and 10-adrs.md.
  • Implementation state (unchanged by this disposition): partially implemented: all three planned specs (OrderLifecycle.tla, ReplaySnapshot.tla in alphaswarm_bots, SpecVersion.tla in alphaswarm_core) shipped the same day and are TLC-verified per specs/README.md; the CI gate (rollout step 2) is not yet wired. Gated on the Architecture Enhancement Guide roadmap (enhancement E1, Wave 1)
  • Authors: Platform team
  • Related: Enhancement Guide §6/E1, ADR 008, ADR 006; Hard Rules 13/15/17/24/41/43/57 (hash-locked spec versions)

Context​

The platform's most safety-critical state machines are guaranteed today only by Python guards plus example-based pytest:

  • the order lifecycle (alphaswarm_bots/execution/lifecycle.py, the _VALID_FORWARD transition table + on_fill over-fill handling);
  • the event-sourced replay loop (ADR 008: append-only bot_events + snapshot anchors + replay_events);
  • hash-locked spec snapshot/resume (SpecPersister.get-or-create-by-hash).

At the time this ADR was written there were zero .tla / .als / PlusCal artifacts in any repository (this is no longer the case — see Status above). Example tests cover the paths the authors thought of; they cannot prove the absence of an illegal interleaving (a duplicate fill that double-counts under target, a replay that diverges from the live fold, a snapshot resume that mutates an existing version). These are exactly the failure modes formal methods are built to catch, and they are the failure modes with real money attached.

The blueprint's four-layer contract stack names this the Temporal-contract layer; the platform is strong on Schema and Protocol contracts and absent on Temporal ones.

Decision​

Adopt machine-checked TLA+ specifications for a deliberately small set of critical state machines, kept faithful to the code, and gate them in CI for the owning module.

  1. Start with OrderLifecycle. Land specs/OrderLifecycle.tla in alphaswarm_bots, transcribing _VALID_FORWARD and on_fill semantics (over-fill → DISPUTED, idempotent re-application keyed on exec_id). The same spec proves the lifecycle (E1) and fill idempotency (E2): modeling fills as a set of distinct exec_ids makes a non-dedup on_fill produce an Apalache counterexample to quantity conservation.
  2. Check safety with Apalache, liveness with TLC. Apalache (symbolic, SMT/Z3) proves inductive invariants for unbounded executions; TLC enumerates small bounded configs for liveness (every order eventually terminal). Invariants: TypeOK, QtyConservation, NoResurrection, IdempotentLedger.
  3. Wire a make spec-check target and a (initially non-blocking) CI job scoped to the bots/execution module; promote to blocking once tooling is pinned.
  4. Keep spec and code in sync with a review-checklist rule: any change to a modeled transition table requires the corresponding spec edit in the same PR.

Scope (and non-scope)​

In scope, in priority order: OrderLifecycle → ReplaySnapshot (ADR 008 projection convergence under partial replay) → SpecVersion (get-or-create is idempotent and never mutates an existing version). Explicitly out of scope: modeling the entire platform, the agent orchestration graph, or anything without real safety/liveness stakes.

Consequences​

Positive

  • Machine-checked safety on the highest-risk transitions, independent of test coverage. The order machine gains a proof that no reachable interleaving violates quantity conservation or resurrects a terminal order.
  • The spec doubles as executable documentation of the FSM and as the source of truth that the Wave-1 Hypothesis state machine mirrors.

Negative / risks

  • TLA+ is a specialist skill; mitigate by keeping specs small and reviewed by a rotating owner.
  • CI tooling (JVM + tla2tools/Apalache) adds a job; keep it module-scoped and cache the toolchain. Start non-blocking to avoid flakiness gating merges.
  • Spec/code drift is a real cost; the same-PR-edit checklist rule mitigates it.

Explicitly rejected

  • Modeling the whole system in TLA+ (cost with no marginal safety on low-risk paths).
  • Replacing runtime guards/tests with specs — specs augment, they do not replace, the Python guards and property tests.

Rollout order​

  1. Done. specs/OrderLifecycle.tla + .cfg + specs/README.md + make spec-check shipped in alphaswarm_bots (2026-06-19).
  2. Non-blocking CI job on bots/execution; promote to blocking after two green weeks. Not yet wired — no spec-check/tla2tools/apalache reference found in alphaswarm_bots/.github/workflows/ as of this review.
  3. Done. ReplaySnapshot.tla (alphaswarm_bots, ADR 008) and SpecVersion.tla (alphaswarm_core) both shipped 2026-06-19 and are TLC-verified per specs/README.md.