Summary / 23. Workflow and state machine / Document
Spec 2026-09-06
Shared copy: the operator's name and machine names are replaced by roles. Nothing else is changed.
Rendering…
# Build Spec 23 — Workflow / State Machine (executable, evidence-gated, deterministic control plane) > Derived from `papers/23-workflow-state-machine.md` — "The Coding Workflow as an Executable, Evidence-Gated State Machine Under a Deterministic Control Plane." > This document drives the build of component 23: the **workflow itself** — the thing that orders the twenty-two capabilities the > harness already owns. By component 22 the harness possesses every individual stage — reconnaissance, localization, impact > analysis, decomposition, generation, editing, execution, tracing, debugging, repair, reflection, candidate generation, test > execution, validation, regression protection, episodic memory, and the independent reviewer. Component 23 is the layer that > *orders* those stages, and the paper's central claim — made structural here — is that this ordering must **not** be emergent. > The workflow must be a **declared, executable state machine** — explicit states, legal transitions, permitted tools, > input/output schemas, entry and exit conditions, retry and rollback paths, and terminal outcomes — advanced by deterministic > evidence wherever possible, with adaptive plan nodes inside controlled states, artifact-dependency tracking that invalidates > and recomputes only affected downstream work, verified upstream state preserved across retries, and LLM calls reserved strictly > for the semantic judgments made *inside* states. The inversion the paper argues for is stated in one sentence and is the > load-bearing rule of this build: **the model must not own planning, must not own workflow, must not own tool choice, must not > own termination, must not own retry, must not own rollback, and must not own the ordering of validation.** All of those are > *state-management problems*, and state management is a problem software solves perfectly and language models solve > approximately, at cost, and without guarantee. A loop that asks the model "what should you do next?" has converted a solved > problem into a probabilistic one; this component exists to *stop asking*. The invariant that governs the entire design, and > that every later section is an elaboration of, is **the L column contains at most one entry**. The entire **control plane** — > the phase graph of states, legal transitions, gate predicates, per-state tool permissions, artifact-freshness and invalidation > tracking, and retry/rollback/termination edges — is deterministic software on CPU holding **zero** learned entries; the single > learned entry is the **semantic judgment inside a state**, bounded reasoning and action within that state's permitted toolset. > And **an empty L column is a permitted, correct state** — a purely deterministic state or gate (a syntax check, a test run, a > freshness recomputation) executes with no model call at all. The paper assembles the evidence in both directions: Agentless's > fixed three-stage localize→repair→validate pipeline (32.00%, 96/300 on SWE-bench Lite, $0.70 average cost, FSE 2025) as the > argument that declared structure beats autonomy, and the traceability literature (Ceka et al., ISSTA 2026) as the measured cost > of the open floor; StateFlow (COLM 2024) separating process grounding from problem solving; CodePlan and Runtime-Structured > Task Decomposition as the artifact-dependency and adaptive-plan machinery; and AFlow, ADAS, GPTSwarm, and DSPy as the tunable > controller, closed by AgentSpec's runtime enforcement and the Clarke–Emerson–Sistla model-checking result that lets the phase > graph be verified exhaustively for reachability, safety, and liveness before it ever runs. This spec pins the paper's design to > exact primitives: the exact `StateContract` schema (required_inputs, permitted_tools[], output_schema, transition_guards[], > failure_transitions[]), the exact `GatePredicate` schema (a boolean condition over artifacts — existence plus threshold tests), > the exact artifact-freshness lattice (the seven named artifacts × the {VALID, STALE} enum × the dependency edges, with the > canonical rule verbatim), the exact D/L invariant, the exact 18 canonical states plus 2 terminal states with an exhaustively > declared transition relation and per-state tool allowlists, the exact retry/rollback/termination edges, the exact model-checking > requirement, the exact honest A/B and ablation protocol, and an exact build sequence. --- ## 1. Purpose & Scope Build a **deterministic workflow control plane plus a bounded semantic-judgment slot** — a finite phase graph that, given a coding task entering at `INIT`, decides *which state comes next*, *which tools are callable in that state*, *which artifacts must be present and what properties they must satisfy before a transition may fire*, *which artifacts a new piece of evidence has made stale and must be recomputed*, and *when the run terminates — accepted or rejected* — all of it deterministic software on CPU, with the model invited in only where a semantic judgment is actually required. The scope is the **workflow layer only**. Components 01–22 own *how* each individual stage is performed; this component owns *who decides what happens next*. The answer it defends is the least glamorous one available: **nobody decides at runtime.** The order of operations is a graph, written down in advance, advanced by evidence, and the model is a called function inside it — an instrument the control plane wields, never the engine that drives it. The paper's discipline compresses into a handful of load-bearing moves that carry the entire design. **Declared, not emergent**: the state set, the transition relation, the gate predicates, the tool allowlists, the freshness lattice, and the retry/rollback/termination edges are all written down in advance, and any transition *not* written down is not expressible — there is no "the model may go anywhere" escape clause, because the transition function is total and closed. **Evidence-gated, not claim-gated**: every transition is guarded by a **gate predicate** — a boolean condition over *artifacts* the harness produced and stored, evaluated by deterministic code, never by the model, and never from prose the model wrote. **Dependency-aware, not rerun-everything**: a freshness lattice over typed artifacts propagates staleness *downstream only*, so new evidence invalidates and recomputes only affected downstream work, and verified upstream state is preserved across retries. **Bounded-L**: the model's freedom is entirely *inside* a state (an unbounded action room scoped to that state's bounded toolset) and entirely *absent* at the boundary — the model never invents a transition, never evaluates its own gate, and never chooses its own tools. Three principles decide every design choice. **P1 The model solves the problem; the graph owns the process.** The coding problem — "what is wrong, and what change makes the tests pass without breaking the contract" — is genuinely semantic and is where the learned model earns its place. The process problem — "after a failed test run, re-localize before regenerating, and never re-run an unaffected downstream stage" — is a finite-state reachability question with a known answer, and forcing the model to re-derive it every turn is a tax that produces only regression toward entropy. **P2 The D/L invariant** — the control plane (states, transitions, gates, tool permissions, freshness, invalidation, retry, rollback, termination) is [D], zero learned entries; the L column holds at most one entry: the semantic judgment inside a state; and **an empty L column is a permitted, correct state** — a syntax check, a test run, or a freshness recomputation advances the workflow with no model call at all. **P3 The graph is model-checkable, not merely testable** — because the phase graph is finite, small, and total, its reachability, safety, and liveness can be *proven* by a model checker before it ever runs; this is the one component whose correctness is a theorem rather than an empirical result. The build lives in `build/23-workflow-state-machine/`, writes nothing into the live harness, and is kept **only if** the state machine strictly dominates its own absence — measured on the honest instruments of §8: resolve rate, tokens, wall time, LLM calls, illegal/redundant actions, repeated work, regressions, and stale-context mistakes, A/B-tested against the free-agent baseline (the emergent loop this component replaces) and against the intermediate ablations (fixed pipeline; + adaptive plan DAG; + artifact invalidation/partial retry). --- ## 2. Round 1 vs later rounds (toward the 100% target) The goal is the paper's full **100%** spec. **~80%** is only the expected **first-round landing**; later rounds climb from there. **BUILD-NOW = the Round 1 build** (rows 1–8); **DEFERRED = later rounds** (rows 9–10), **not excluded** but gated by the same §8 A/B protocol. Every later round of this component still builds within the same `build/23-workflow-state-machine/` tree. | # | Component (paper §3/§4/§5/§6) | Classification | |---|---|---| | 1 | State registry + transition table — the 18 canonical states + 2 terminal states, and the exhaustively declared `(state, state)` transition relation (§3.1) | **BUILD-NOW** | | 2 | Gate-predicate engine — boolean conditions over artifacts (existence + threshold tests), harness-evaluated (§3.2) | **BUILD-NOW** | | 3 | Per-state tool allowlists — the exact toolset callable per state; off-list = `ILLEGAL_TOOL` (§3.3) | **BUILD-NOW** | | 4 | Artifact freshness lattice + invalidation — the seven named artifacts × {VALID, STALE} + downstream-only dependency edges (§4.2) | **BUILD-NOW** | | 5 | Retry / rollback / termination edges — first-class graph edges carrying typed artifacts (§3.4) | **BUILD-NOW** | | 6 | Model-call contract — the single bounded L entry per state, typed output schema, toolset-scoped (§5) | **BUILD-NOW** | | 7 | Model-checker harness — reachability, safety, liveness verified exhaustively before the graph runs (§6.4) | **BUILD-NOW** | | 8 | Fault-injection + A/B driver — free-agent baseline vs fixed pipeline vs state machine vs +adaptive-plan vs +invalidation/partial-retry (§7, §8) | **BUILD-NOW** | | 9 | **Offline graph tuning (AFlow / GPTSwarm / ADAS / DSPy)** — search and compile the graph's shape, node prompts, and edge connectivity against a metric, at design time only (§6.1) | **DEFERRED** — Round 1 ships the hand-declared graph; graph-search tuning is adopted only if it strictly dominates the declared graph on §8's measures, and is performed offline, never at runtime | | 10 | **Adaptive plan DAG refinement (CodePlan-style)** — the plan as a first-class dependency-aware artifact that re-plans when an edit diverges from the plan's assumption (§4.1) | **DEFERRED** — Round 1 ships the static plan node with the freshness lattice; full adaptive re-planning inside `PLAN` is added only if it strictly dominates on §8's measures | **The cost rule (explicit).** The L column holds at most one entry — the semantic judgment inside a state — and nothing else. In Round 1 that entry is produced by the harness's own weak model (`deepseek-v4-pro`) on exactly the same terms as the happy path; it is **not** a new learned node, and it is **not** trained. The model is handed the state's required inputs and asked to emit the state's typed output within the state's tool allowlist; its cost is bounded to one model call per state (or a strictly bounded short sequence, each schema-validated), and it never decides *which state is next*, *whether a gate opens*, *which tools it may use*, *whether to retry, roll back, or terminate*, or *whether its own output satisfies the schema* — those are all deterministic. The DEFERRED rows (offline graph tuning, adaptive plan DAG) must clear the same bar as in every other component: strictly dominate the deterministic baseline on §8's measures, on held-out tasks, at a defensible cost, or be rejected. **Design decision: DETERMINISTIC-FIRST, SINGLE-L.** Round 1 puts no model anywhere in the control plane — not in state selection, not in gate evaluation, not in tool enforcement, not in freshness propagation, not in retry/rollback/termination choice, not in model checking. The full deterministic control plane (rows 1–5, 7) is the build; the single L entry is the semantic judgment inside a state, produced only *after* the deterministic control plane has entered that state, declared its required inputs and output schema, and enforced its tool allowlist. --- ## 3. The Deterministic Control Plane (D) The control plane is a finite graph, and it is where the paper's "deterministic software on CPU" becomes software. Every function in this section is deterministic; the L column contributes nothing here, and the invariant is stated at the outset of the architecture and re-stated at its close: **the L column contains at most one entry**, and at this layer it is exactly zero — **an empty L column is a permitted, correct state**, and it is the *common* state, not the exceptional one. Concretely, the control plane's pipeline is: ``` TASK ENTERS at INIT → state registry + transition table [D] → the 18+2 states, the exhaustive (state, state) edge set (§3.1) → gate-predicate engine [D] → boolean conditions over artifacts; existence + threshold tests (§3.2) → per-state tool allowlists [D] → exact toolset per state; off-list = ILLEGAL_TOOL (§3.3) → artifact freshness lattice [D] → VALID/STALE status + downstream-only invalidation (§4.2) → retry / rollback / termination [D] → first-class edges carrying typed artifacts (§3.4) → model-checker harness [D] → reachability, safety, liveness proven before it runs (§6.4) → (L) semantic judgment inside state → the at-most-one learned entry: one bounded call → typed output (§5) ``` The model never decides what state comes next (the graph does), never evaluates a gate (the predicate engine does), never chooses its tools (the allowlist does), never propagates staleness (the lattice does), never chooses an edge on failure (the declared retry/rollback/termination edges do), and never verifies the graph (the model checker does). All artifacts land in `build/23-workflow-state-machine/`. ### 3.1 States, legal transitions, and terminal outcomes [D] A **state** is a named phase of the workflow, each one corresponding to a component the harness already owns. The canonical set, in dependency order, is **18 states plus 2 terminal states**: `INIT`, `RECONNAISSANCE` (repository manifest and context retrieval), `LOCALIZE` (fault localization), `IMPACT` (dependency impact analysis), `PLAN` (task decomposition), `GENERATE` (patch/code generation), `EDIT` (the editing mechanism), `EXECUTE` (code execution), `TRACE` (runtime instrumentation), `DEBUG` (error interpretation), `REPAIR` (iterative repair), `REFLECT` (post-failure reflection), `CANDIDATES` (competing-hypothesis generation), `TEST` (test execution), `VALIDATE` (patch acceptance), `REGRESSION` (regression protection), `MEMORIZE` (episodic memory write), `REVIEW` (the independent reviewer) — and the two terminal sinks `TERMINAL_ACCEPT` and `TERMINAL_REJECT`. A **legal transition** is an enumerated edge in the graph. The transition relation is declared **exhaustively** — the set of `(state, state)` pairs is written down, and any pair *not* written down is not expressible. There is no "the model may go anywhere" escape clause; the transition function is total and closed. The terminal states are sinks: no edge leaves `TERMINAL_ACCEPT` or `TERMINAL_REJECT`. This is the paper's workflow net (van der Aalst's Petri-net lineage, refined with the *Workflow Patterns* control-flow idioms), with two modern refinements: its transitions are guarded by *data conditions* (the gate predicates of §3.2) rather than pure control flow, and its tokens are *typed artifacts* (§4) rather than anonymous marks. The legal transition relation, declared exhaustively and classified, is: **FORWARD edges (happy path, dependency order).** `INIT → RECONNAISSANCE` · `RECONNAISSANCE → LOCALIZE` · `LOCALIZE → IMPACT` · `IMPACT → PLAN` · `PLAN → GENERATE` · `GENERATE → EDIT` · `EDIT → EXECUTE` · `EXECUTE → TRACE` · `TRACE → DEBUG` · `DEBUG → REPAIR` · `DEBUG → REFLECT` · `REFLECT → CANDIDATES` · `CANDIDATES → REPAIR` · `CANDIDATES → PLAN` · `EXECUTE → TEST` · `TEST → VALIDATE` · `VALIDATE → REGRESSION` · `REGRESSION → MEMORIZE` · `MEMORIZE → REVIEW` · `REVIEW → TERMINAL_ACCEPT`. **RETRY edges (the canonical inner cycle `TEST → REPAIR → EDIT → EXECUTE → TEST`).** `TEST → REPAIR` (tests failed) · `REPAIR → EDIT` (repair produced a patch) · `EDIT → EXECUTE` (the edit mechanism re-enters execution) · `EXECUTE → TEST` (execution re-enters the test run). A retry edge is taken when the gate predicate at the head of the cycle is still false but a bounded retry budget remains. **ROLLBACK edges (return to an earlier *verified* state, carrying preserved artifacts forward).** `VALIDATE → LOCALIZE` (validation failure implicates the diagnosis rather than the patch — returns with `RepoManifest` and `LocalizationResult` still VALID) · `VALIDATE → REPAIR` (validation failure implicates the patch, not the diagnosis) · `REVIEW → REPAIR` (the independent reviewer surfaces a verified defect that implicates the patch) · `REGRESSION → REPAIR` (a regression was detected). **TERMINATION edges (a decision the graph makes, on declared evidence — never the model's).** `PLAN → TERMINAL_REJECT` (contradiction-in-specification: no satisfiable plan) · `TEST → TERMINAL_REJECT` (out-of-budget: retry budget exhausted) · `EXECUTE → TERMINAL_REJECT` (unrecoverable-sandbox-failure) · `VALIDATE → TERMINAL_REJECT` (contradiction or unrecoverable validation failure) · `REVIEW → TERMINAL_REJECT` (a verified defect that is unrepairable, or out-of-budget). The three named variants — **out-of-budget**, **contradiction-in-specification**, **unrecoverable-sandbox-failure** — are the termination reasons recorded on the edge. Any `(state, state)` pair not enumerated above is **not expressible**. An attempt to traverse it is an `ILLEGAL_TRANSITION` event, rejected at the boundary and logged — never honored, never interpreted, never "helpfully" routed. ### 3.2 Gate predicates: evidence-driven, harness-executed [D] Every transition is guarded by a **gate predicate** — a boolean condition over *artifacts*, evaluated by the harness, never by the model. The canonical form is a conjunction over artifact existence and threshold tests: > `LocalizationResult exists AND top-candidate confidence > threshold` The predicate names an artifact (`LocalizationResult`), asserts it exists, and tests a property of it against a threshold. Three properties make it a gate rather than a suggestion, and they are load-bearing: - **It is evidence-driven.** The predicate reads an artifact the harness produced and stored, not a claim the model made in prose. "The model says it localized the fault" is not evidence; "a `LocalizationResult` record with a top candidate and a confidence is present" is evidence. The gate checks the latter. - **It is harness-executed.** The predicate is evaluated by deterministic code at the moment the transition is considered. The model never evaluates its own gate; indeed the model never *sees* the gate. The model produces output inside a state; the harness decides whether that output opened the door to the next state. - **It is falsifiable and inspectable.** Because the predicate is a deterministic function of stored artifacts, the answer to "why did the workflow leave `LOCALIZE`?" is always "because this predicate was true over these artifacts," and that answer can be logged, replayed, and stepped through. The gate is the mechanism by which "deterministic evidence advances the workflow whenever possible" becomes an actual property of the system rather than a slogan. Its schema is pinned exactly in §4.2. ### 3.3 Per-state tool permissions [D] Each state carries a **tool allowlist**: the exact set of tools callable from within that state. The `EXECUTE` state may call the sandbox executor; it may not call the patch generator. The `GENERATE` state may call retrieval tools; it may not call the test runner (it has nothing validated to test). A model operating inside a state can invoke *any* tool on that state's list and *no* tool off it; an off-list invocation is not routed to the tool at all — it is rejected at the boundary as an `ILLEGAL_TOOL` event. Tool choice, like workflow choice, is therefore not a model decision; it is a *state property*. The model's freedom is real but always scoped to the room it is standing in. The full allowlist table is pinned in §4.4. ### 3.4 Failure, re-entry, and termination as first-class edges [D] In an emergent workflow, failure is an exception — something the model must notice and react to, or fail to notice and corrupt. In the phase graph, failure is an *edge*. Three classes of non-happy-path edges are declared alongside the happy path: **retry edges** (loops within a state or between a state and its immediate repair predecessor — the canonical inner cycle `TEST → REPAIR → EDIT → EXECUTE → TEST`, taken when the gate at the head of the cycle is still false but a bounded retry budget remains); **rollback edges** (returns to an earlier *verified* state, carrying its preserved artifacts forward — when `VALIDATE` fails in a way that implicates the diagnosis rather than the patch, the rollback edge returns to `LOCALIZE`, critically with the repository manifest and localization artifacts still **VALID**, so the recomputation is scoped to what actually changed); and **termination edges** (edges to `TERMINAL_REJECT` and their variants — out-of-budget, contradiction-in-specification, unrecoverable-sandbox-failure; termination is a *decision the graph makes* on declared evidence, never a decision the model makes or forgets to make). These edges are fully specified in §6. The key property, repeated from §1, is **preserve verified upstream state across retries**: a retry or rollback never invalidates an upstream artifact that the failure did not touch. The graph's edges carry typed artifacts, and only the downstream of a change is recomputed. That is the subject of §4. ### 3.5 This layer is [D], and the L column is empty here Every element of §3 — the state set, the transition relation, the gate predicates, the tool allowlists, the retry/rollback/ termination edges, the artifact registry — is deterministic software on CPU. No learned model is consulted to advance a token through the graph, to evaluate a gate, to enforce a tool boundary, or to choose an edge. Recapitulating the invariant: > **the L column contains at most one entry.** And at this layer it is exactly zero. **An empty L column is a permitted, correct state** — and it is the *common* state, not the exceptional one. A syntax-check gate between `EDIT` and `EXECUTE` runs with no model call; a freshness recomputation after a diagnosis change (§4.2) runs with no model call; a bounded retry that re-enters `TEST` runs its transition machinery with no model call. The model is *not* the engine of the workflow. It is a called function. --- ## 4. The Core Schemas (the build's JSON contracts) The following schemas are the load-bearing contracts of the build. Their shapes are EXACTLY these fields, no more and no fewer, and the label "EXACTLY these fields" is itself part of the contract — a field added for convenience is a spec violation. ### 4.1 The StateContract record (EXACTLY these fields) Every one of the 18 canonical states (and both terminal sinks) is declared by a `StateContract`. The paper's description of a state — required inputs, permitted tools, the typed output it must produce, the guarded transitions that leave it, and the failure transitions taken when a guard fails — compiles to exactly these five fields. A state is *only* enterable when every `required_inputs` artifact is VALID (this is how "no `GENERATE` without a VALID `Diagnosis`" becomes structural, not advisory). ```json StateContract { required_inputs: string[] // artifacts that must be VALID for this state to be enterable (e.g. ["Diagnosis"]) permitted_tools: string[] // the exact tool allowlist; an off-list call is ILLEGAL_TOOL, rejected at the boundary output_schema: object // the typed artifact schema this state must emit before any guard may open (name + required fields) transition_guards: GatePredicate[][] // one conjunction (AND) per outgoing edge; each is a list of GatePredicates (§4.2) failure_transitions: Transition[] // retry / rollback / termination edges taken when a guard fails (§4.3) } ``` The load-bearing decisions, enforced not advisory: - **`required_inputs` is a VALID-artifact precondition, checked by the lattice (§4.4), not by the model.** A state whose required inputs include a STALE artifact is not enterable until the lattice recomputes that artifact to VALID. This is the safety property of §6.4 made mechanical. - **`permitted_tools` is a closed allowlist.** The model may call any tool on the list, no tool off it; an off-list invocation is an `ILLEGAL_TOOL` event, never routed. The model never extends its own list. - **`output_schema` is the contract the model's L entry must fill.** The deterministic layer validates the state's output against the schema; a malformed output is re-requested under a bounded retry, then the state is failed deterministically. - **`transition_guards` is a conjunction-per-edge.** Each outgoing edge carries its own guard; the edge whose guard is the first to evaluate true is the edge taken. Guards are evaluated in declared order, deterministically. - **`failure_transitions` is declared, not discovered.** When every forward guard is false, the state's declared failure transitions (retry, rollback, termination) are consulted in order — never the model's judgment. ### 4.2 The GatePredicate record (EXACTLY these fields) The gate predicate is the paper's "boolean condition over artifacts" made exact. A full gate is a **conjunction** (AND) of `GatePredicate` records, each one an artifact-existence assertion plus a single threshold test. The canonical paper example — `LocalizationResult exists AND top-candidate confidence > threshold` — is exactly two `GatePredicate` records ANDed: one asserting existence, one asserting the threshold test. ```json GatePredicate { artifact: string // the named artifact this predicate reads (e.g. "LocalizationResult") — existence is asserted property: string // the artifact property under test (e.g. "top_candidate_confidence") operator: enum // {GT, GTE, LT, LTE, EQ, NEQ} threshold: float // the threshold the property is compared against } ``` Three properties are structural, and they must hold mechanically: - **Evidence-driven.** The predicate reads an artifact the harness produced and stored, never a claim the model made in prose. - **Harness-executed.** The predicate is evaluated by deterministic code at the moment the transition is considered; the model never evaluates its own gate, and never sees it. - **Falsifiable and inspectable.** The predicate is a deterministic function of stored artifacts, so "why did the workflow leave `LOCALIZE`?" always has a logged, replayable, step-through-able answer. ### 4.3 The Transition record (EXACTLY these fields) The transition relation of §3.1 is stored as a set of `Transition` records — one per enumerated edge. The field set makes the "total and closed" property checkable: the registry is the *entire* expressible relation, and an edge not present is not expressible. ```json Transition { from: string // source state to: string // destination state kind: enum // {forward, retry, rollback, termination} guard: GatePredicate[] // the conjunction of gate predicates that must hold for this edge (empty = unconditional) reason: string // for termination edges: {out_of_budget, contradiction_in_specification, unrecoverable_sandbox_failure} } ``` ### 4.4 The artifact freshness lattice (EXACTLY these fields) The harness formalizes CodePlan's insight as a **freshness lattice** over its typed artifacts. Exactly **seven** artifacts are named by the paper as carrying freshness status: `RepoManifest`, `LocalizationResult`, `Diagnosis`, `Plan`, `Patch`, `Review`, `ValidationResult`. Each carries a freshness status — **VALID** or **STALE** — and a set of dependency edges recording which artifacts it is downstream of. A change propagates staleness **downstream only**: staleness is a directed, transitive property along the dependency edges, and recomputation is triggered *only* for STALE nodes. Nothing upstream is ever re-run because something downstream changed; that would be recomputing a function whose inputs did not change. ```json ArtifactFreshness { artifact: string // one of the seven named lattice artifacts, named exactly freshness: enum // {VALID, STALE} depends_on: string[] // upstream artifacts this one was computed from (dependency edges, downstream-only propagation) } ``` The seven lattice nodes, with their dependency edges declared: ```json [ { "artifact": "RepoManifest", "freshness": "VALID", "depends_on": [] }, { "artifact": "LocalizationResult","freshness": "VALID", "depends_on": ["RepoManifest"] }, { "artifact": "Diagnosis", "freshness": "VALID", "depends_on": ["RepoManifest", "LocalizationResult"] }, { "artifact": "Plan", "freshness": "VALID", "depends_on": ["Diagnosis"] }, { "artifact": "Patch", "freshness": "VALID", "depends_on": ["Diagnosis", "Plan"] }, { "artifact": "Review", "freshness": "VALID", "depends_on": ["Patch"] }, { "artifact": "ValidationResult", "freshness": "VALID", "depends_on": ["Patch", "Review"] } ] ``` The canonical rule, stated by the paper as a rule and pinned here **verbatim** (read it as an arrow, not a sentence): > **Diagnosis changes → Patch / Review / Validation become STALE; RepoManifest / Localization stay VALID.** When a new failure trace forces the `Diagnosis` to be revised, the artifacts computed *from* the diagnosis — the `Patch`, the `Review` of that patch, the `ValidationResult` of that patch (the paper's "Validation" ≡ the lattice's `ValidationResult`) — are marked STALE and must be recomputed. The artifacts the diagnosis was computed *from* — the `RepoManifest` and the `LocalizationResult` — are upstream, were not touched by the revision, and remain VALID. This is the precise mechanism by which "new evidence invalidates and recomputes only affected downstream work" is enforced. The recomputation itself — marking nodes stale, topologically ordering the recomputation, and re-running the affected states' deterministic gates — is deterministic software [D]; only when a recomputation reaches a state whose *content* requires a semantic judgment does the L column get its single entry (§5). ### 4.5 Per-state tool allowlists (the exact vocabulary) The tool vocabulary is the harness's own stage primitives (components 01–22), addressed by stable names. The allowlist per state is EXACTLY this set, and an off-list call is `ILLEGAL_TOOL`: | State | permitted_tools[] | |---|---| | `INIT` | `[]` (no tools; the run opens) | | `RECONNAISSANCE` | `repo.manifest`, `code.graph` | | `LOCALIZE` | `code.graph`, `trace.read` | | `IMPACT` | `impact.analyze`, `code.graph` | | `PLAN` | `task.decompose` | | `GENERATE` | `patch.generate`, `code.graph`, `repo.manifest` (retrieval tools; **not** `test.run`) | | `EDIT` | `edit.apply` | | `EXECUTE` | `sandbox.execute` (**not** `patch.generate`) | | `TRACE` | `trace.instrument`, `sandbox.execute` | | `DEBUG` | `error.interpret`, `trace.read` | | `REPAIR` | `repair.iterative`, `patch.generate`, `edit.apply` | | `REFLECT` | `reflect.failure`, `trace.read` | | `CANDIDATES` | `candidates.generate` | | `TEST` | `test.run` (**not** `patch.generate`) | | `VALIDATE` | `validate.accept`, `test.run` | | `REGRESSION` | `regression.check`, `test.run` | | `MEMORIZE` | `memory.write` | | `REVIEW` | `review.critic` | | `TERMINAL_ACCEPT` | `[]` (sink) | | `TERMINAL_REJECT` | `[]` (sink) | The per-state `output_schema` maps to the typed artifacts: `RECONNAISSANCE → RepoManifest`, `LOCALIZE → LocalizationResult`, `IMPACT → ImpactResult` (dependency-impact evidence; an input to `Plan`/`Diagnosis`, not itself a lattice node), `PLAN → Plan`, `GENERATE/EDIT/REPAIR → Patch`, `EXECUTE → ExecutionResult`, `TRACE → Trace`, `DEBUG → Diagnosis`, `REFLECT → Reflection`, `CANDIDATES → CandidateSet`, `TEST → TestResult`, `VALIDATE → ValidationResult`, `REGRESSION → RegressionResult`, `MEMORIZE → MemoryWrite`, `REVIEW → Review`. The seven lattice artifacts are the ones whose staleness matters for recomputation; the remaining outputs are scoped ephemera consumed within the state or folded into a lattice node's inputs. --- ## 5. The L Column — the semantic judgment inside a state (AT MOST ONE entry) The model's entire role in this component is the semantic judgment made *inside* a state: bounded reasoning and action within that state's permitted toolset, producing the typed output that state's schema demands. This section specifies exactly what it is permitted to be, what it outputs, and what it is forbidden to do. **The model is a called function, not the engine.** It is handed the state's `required_inputs` (all VALID, per §4.1) and asked to emit the state's `output_schema` within the state's `permitted_tools`. Inside a state it may freely interleave reasoning and action — ReAct's Thought→Action→Observation loop is kept, but *demoted*: in `LOCALIZE` it may think, probe the code graph, read a trace, think again, and re-probe, as many times as the state's budget allows. What it may **never** do is *invent a transition*. A ReAct-style trajectory that tries to leave the state — that, for example, attempts to call a `GENERATE`-state tool while still in `LOCALIZE` — is not honored, not interpreted, not "helpfully" routed; it is rejected as `ILLEGAL_TRANSITION`, and the harness advances (or does not advance) according to the graph and its gates alone. The phrase deserves the emphasis: **the model never invents a transition.** Every edge is declared (§3.1); every gate is harness-executed (§3.2). The model's freedom is entirely *inside* the state — an unbounded action room scoped to a bounded toolset — and entirely *absent* at the boundary. **One bounded model call.** The single [L] entry is one bounded model call, or a short bounded sequence of calls, each producing the typed output that state's schema demands and each exercising only that state's toolset. It never outvotes deterministic evidence, because it is never given a vote to cast. It never decides *which state is next*, *whether a gate opens*, *which tools it may use*, *whether to retry, roll back, or terminate*, or *whether its output satisfies the schema* — those are all deterministic. Recapitulating the invariant at its tightest form: > **the L column contains at most one entry.** The control plane — states, transitions, gates, tool permissions, freshness, invalidation, retry, rollback, termination — is [D], zero learned entries. The single [L] entry is the **semantic judgment inside a state**: one bounded model call, or a short bounded sequence of calls, each producing the typed output that state's schema demands, and each exercising only that state's toolset. Tree-search variants such as LATS sit comfortably *inside* this picture: they are controlled-search strategies over a state's bounded action space, still gated and still scoped by the graph, not a license for the model to own its own process. ### 5.1 The empty L column When a state is purely deterministic — a syntax check, a test run, a freshness recomputation, a topological re-order — the L column is empty, and **an empty L column is a permitted, correct state.** That emptiness is not a gap in the architecture; it is the architecture correctly declining to spawn a learned entry where none earns its cost. The control plane runs whether or not the L column has an entry; the L entry never runs without the control plane. **the L column contains at most one entry** — and **an empty L column is a permitted, correct state**: the model is, in CoALA's terms, a component of the decision procedure; it is never the decision procedure. --- ## 6. Retry / Rollback / Termination as first-class edges In an emergent workflow, failure is an exception — something the model must notice and react to, or fail to notice and corrupt. In the phase graph, failure is an **edge**, and the three classes are first-class, declared alongside the happy path. ### 6.1 Retry edges — the canonical inner cycle The canonical inner cycle is **`TEST → REPAIR → EDIT → EXECUTE → TEST`**. A retry edge is taken when the gate predicate at the head of the cycle is still false (the tests are still failing) but a bounded retry budget remains. The retry budget is a deterministic counter, not a model judgment: each traversal of a retry edge decrements the budget, and when the budget is exhausted the graph takes the declared termination edge (`TEST → TERMINAL_REJECT`, reason `out_of_budget`). The model never decides to retry and never decides to stop retrying. ### 6.2 Rollback edges — preserve verified upstream state Rollback edges return to an earlier *verified* state, carrying its preserved artifacts forward. When `VALIDATE` fails in a way that implicates the diagnosis rather than the patch, the rollback edge `VALIDATE → LOCALIZE` is taken — but, critically, it returns with the repository manifest and localization artifacts still **VALID**, so the recomputation is scoped to what actually changed. When the failure implicates the patch rather than the diagnosis, the rollback edge `VALIDATE → REPAIR` is taken. The mechanism by which this preservation is guaranteed is the freshness lattice of §4.4: a rollback edge invalidates only the downstream of the implicated artifact, never its upstream. **A retry or rollback never invalidates an upstream artifact that the failure did not touch.** The graph's edges carry typed artifacts, and only the downstream of a change is recomputed. ### 6.3 Termination edges — a graph decision, not a model decision Termination is a *decision the graph makes*, on declared evidence, never a decision the model makes or forgets to make. The termination edges of §3.1 carry a `reason` field enumerating the three named variants — **out-of-budget**, **contradiction-in-specification**, **unrecoverable-sandbox-failure** — and they all land in `TERMINAL_REJECT`. The happy-path termination is `REVIEW → TERMINAL_ACCEPT`, taken only when the independent reviewer surfaces no verified defect and the deterministic validation policy accepts. Both terminal states are sinks: no edge leaves them. A run that reaches either is finished; a run that reaches neither cannot exist, because liveness (§7) is a proven property of the graph. --- ## 7. The model-checking requirement (before it runs) The final property is the one that makes this component categorically different from its twenty-two predecessors. Clarke, Emerson, and Sistla established that a finite-state system's correctness against temporal-logic specifications — **reachability, safety, liveness** — is mechanically decidable: model checking. The phase graph is finite, small, and total. That means it is **the one component small enough to model-check exhaustively** before it ever runs. Every other component's correctness is empirical; the phase graph's correctness is a theorem. Three queries must be verified before the graph is allowed to run, each answered by the model checker in milliseconds, *not* by running the harness and hoping: 1. **Reachability** — "can `TERMINAL_REJECT` be reached from `INIT` on some artifact valuation?" It must be reachable, or the harness can hang. (And symmetrically: is `TERMINAL_ACCEPT` reachable from `INIT`? It must be, or the happy path is dead.) 2. **Safety** — "can the graph ever enter `GENERATE` without a VALID `Diagnosis`?" It must not. This is the `required_inputs` precondition of §4.1 lifted to a temporal property, checked over the whole graph, not asserted per-state. 3. **Liveness** — "does every non-terminal state have a path to a terminal state?" It must, or a live-lock exists. (A state that can only loop forever is a dead task in van der Aalst's soundness terms, and it is a model-checker finding, not a runtime surprise.) The model checker is a deterministic harness [D], run at build time and re-run on any change to the state registry or transition table. A graph that fails any of the three queries is not shipped — the build is red until the query is green. This is the concrete payoff of making the control plane a deterministic finite graph: the one thing that most deserves a guarantee is the one thing that can actually get one. --- ## 8. Honest measurement — A/B and ablation A component whose whole premise is "stop asking the model to manage its own process" must hold *itself* to the same standard: measured, not asserted. This section specifies how the state machine's value — or lack of it — is measured, so the component earns its place in the harness by evidence rather than by assertion. ### 8.1 The baseline and the arms The **baseline is the free-agent (emergent loop)** — the ReAct-style open floor this component exists to replace, where the model owns its own next-step, tool choice, retry, and termination. Against that baseline, four arms are compared, each a strict superset of the last so the marginal value of each mechanism is isolable: 1. **Fixed pipeline** — the declared states and transitions, no freshness lattice, no adaptive plan, no invalidation. (This is the Agentless-style argument: three-to-twenty declared stages, but rerun-everything on any failure.) 2. **State machine** — arm 1 plus the full gate-predicate engine and per-state tool allowlists and retry/rollback/termination edges, still without the freshness lattice. 3. **State machine + adaptive plan DAG** — arm 2 plus the plan as a dependency-aware artifact that re-plans inside `PLAN` when an edit diverges from the plan's assumption (the CodePlan-style machinery). 4. **State machine + artifact invalidation / partial retry** — arm 2 (or arm 3) plus the freshness lattice of §4.4: staleness propagates downstream-only, and a retry re-runs only the STALE subgraph, never the verified upstream. The full component is arm 4. The arms isolate exactly the paper's claims: 1 vs baseline isolates "declared structure beats autonomy"; 2 vs 1 isolates "gates + allowlists + first-class failure edges"; 3 vs 2 isolates "adaptive planning"; 4 vs 2 isolates "invalidation / partial retry". ### 8.2 The instruments (never "did it sound good") Every arm is measured on the same held-out task population, same model (`deepseek-v4-pro`), same hardware, with these instruments — all deterministic counters and timers, never a self-report: 1. **Resolve rate** — the fraction of held-out tasks reaching `TERMINAL_ACCEPT` (for arms; for the free-agent baseline, the fraction resolved by its own emergent criterion). 2. **Tokens** — total model tokens consumed across the run (the budget the L column actually spent). 3. **Wall time** — end-to-end latency. 4. **LLM calls** — the number of model calls made (the L column's cardinality, which the invariant bounds to at most one *per state*, and zero for purely deterministic states). 5. **Illegal actions** — `ILLEGAL_TRANSITION` + `ILLEGAL_TOOL` events (should be zero for all state-machine arms by construction, and nonzero for the free-agent baseline; a nonzero count in a state-machine arm is a build defect). 6. **Redundant actions** — repeated identical tool calls within/across states (the open floor's hallmark). 7. **Repeated work** — recomputation of artifacts that were already VALID (the freshness lattice drives this toward zero; arms 1–2 without the lattice should show it, arms 3–4 should not). 8. **Regressions** — introduced regressions caught at `REGRESSION`/`VALIDATE` (a patch that broke a pinned contract). 9. **Stale-context mistakes** — decisions made on an artifact that had been invalidated but not recomputed (arm 4 should show zero by construction; arms 1–2 should show it). ### 8.3 A/B decision rule (explicit) The state machine is **kept iff** arm 4 strictly dominates the free-agent baseline on the instruments that matter — resolve rate and repeated work and illegal actions and stale-context mistakes — at no worse tokens/wall time than the baseline's own cost, measured on held-out tasks. Each intermediate arm (1, 2, 3) is likewise kept only if it strictly dominates the arm before it on at least one instrument and degrades none beyond noise. A mechanism whose *addition* degrades a measure is a demonstrated harm and is removed outright. **Never keep a mechanism because it sounds rigorous.** If arm 4 is statistically indistinguishable from the free-agent baseline, the invariant's escape hatch fires: **an empty L column is a permitted, correct state**, and the machinery is pared back until the evidence changes. ### 8.4 Ablation rule (mechanical) The instrument that enforces "keep the mechanism only if it strictly dominates its absence" mechanically. One mechanism removed at a time, everything else held fixed, the delta measured on the instruments of §8.2: 1. **Ablate the gate predicates** (let transitions fire unconditionally) — the direct test of the evidence-gated claim. The delta must show illegal/redundant actions and stale-context mistakes rising. 2. **Ablate the tool allowlists** (let the model call any tool from any state) — the direct test of the "tool choice is a state property" claim. The delta must show `ILLEGAL_TOOL` — which the ablated arm can no longer even *count* — replaced by redundant cross-state tool calls and repeated work. 3. **Ablate the freshness lattice** (rerun everything on any failure) — the direct test of the "recompute only affected downstream" claim. The delta must show repeated work and tokens and wall time rising with no resolve-rate gain. 4. **Ablate the retry/rollback/termination edges** (let the model decide what to do on failure) — the direct test of the "failure is an edge, not an exception" claim. The delta must show the baseline's emergent-failure pathologies returning: stuck loops, un-terminated runs, and stale-context mistakes. 5. **Ablate the single-L contract** (let the model own next-step/tool/termination) — the direct test of the entire D/L invariant. The delta must show the free-agent baseline's full cost profile returning: more tokens, more wall time, more illegal and redundant actions, lower resolve rate. A mechanism is **DELETED** iff its removal does **not** degrade the honest measures beyond noise. The L column is never granted a second entry to "fix" a problem a deterministic mechanism can solve — that would be re-importing the open floor through the back door. --- ## 9. Implementation Order (build sequence) Eight phases, each independently testable and reversible, landing in `build/23-workflow-state-machine/` as standalone importable modules. The order is deliberate — it builds the deterministic control plane from the state registry outward, in the exact sequence the paper's mechanics require: **state registry + transition table first, then the gate-predicate engine, then the per-state tool allowlists, then the artifact freshness lattice + invalidation, then the retry/rollback/termination edges, then the model-call contract, then the model-checker harness, then the fault-injection + A/B driver.** Rollback = delete or flag-off that phase's module; nothing earlier breaks because phases only add modules and never mutate live harness code. | Phase | Delivers | Isolated test | Rollback | |---|---|---|---| | **1. State registry + transition table** | `states.py` (§3.1 the 18 canonical states + 2 terminal sinks; the exhaustive `(state, state)` relation classified forward/retry/rollback/termination) | Assert the state set is exactly the 18+2 names; assert the relation is total and closed (no un-enumerated pair expressible); assert terminal states are sinks (no outgoing edge); assert the retry cycle `TEST→REPAIR→EDIT→EXECUTE→TEST` is present; assert **no LLM consulted**. | Delete `states.py`. | | **2. Gate-predicate engine** | `gates.py` (§3.2 the `GatePredicate` schema + the conjunction evaluator over stored artifacts) | Evaluate the canonical gate `LocalizationResult exists AND top-candidate confidence > threshold` against a fixture with/without the artifact and with confidence above/below threshold; assert the result is a pure function of artifacts; assert **no LLM consulted**. | Delete `gates.py`. | | **3. Per-state tool allowlists** | `allowlist.py` (§3.3/§4.5 the exact toolset per state; off-list = `ILLEGAL_TOOL`) | Assert `EXECUTE` cannot call `patch.generate`; assert `GENERATE` cannot call `test.run`; assert every state's list is a subset of the tool vocabulary; assert an off-list invocation raises `ILLEGAL_TOOL` and is not routed; assert **no LLM consulted**. | Delete `allowlist.py`. | | **4. Artifact freshness lattice + invalidation** | `freshness.py` (§4.4 the seven named artifacts × {VALID, STALE} + downstream-only dependency edges) | Change `Diagnosis`; assert `Patch`/`Review`/`ValidationResult` become STALE while `RepoManifest`/`LocalizationResult` stay VALID; assert staleness propagates downstream-only and transitively; assert recomputation is triggered only for STALE nodes; assert **no LLM consulted**. | Delete `freshness.py`. | | **5. Retry / rollback / termination edges** | `edges.py` (§3.4/§6 first-class failure edges carrying typed artifacts) | Force a `TEST` failure with retry budget remaining → assert `TEST→REPAIR` taken; exhaust the budget → assert `TEST→TERMINAL_REJECT` (reason `out_of_budget`); force a diagnosis-implicating `VALIDATE` failure → assert `VALIDATE→LOCALIZE` with `RepoManifest`/`LocalizationResult` still VALID; assert **no LLM consulted**. | Delete `edges.py`. | | **6. Model-call contract** | `slot.py` (§5 the single bounded L entry per state: required_inputs → typed output within permitted_tools) | Run one bounded model call in `LOCALIZE`; assert it emits the typed output, cannot call an off-list tool (`ILLEGAL_TOOL`), cannot invent a transition (`ILLEGAL_TRANSITION`); assert a malformed output is re-requested under bounded retry then the state failed deterministically; assert the L column holds exactly one entry per state (zero for a deterministic state). | Delete `slot.py`. | | **7. Model-checker harness** | `modelcheck.py` (§7 reachability / safety / liveness over the state registry + transition table) | Assert `TERMINAL_REJECT` is reachable from `INIT`; assert no `GENERATE` is enterable without a VALID `Diagnosis`; assert every non-terminal state has a path to a terminal state; assert the checker runs in milliseconds and does not execute the harness; assert **no LLM consulted**. | Delete `modelcheck.py`. | | **8. Fault-injection + A/B driver** | `ab.py` (§8 the free-agent baseline vs the four arms; the nine instruments) | Run the identical held-out population across baseline + 4 arms; report resolve rate, tokens, wall time, LLM calls, illegal/redundant actions, repeated work, regressions, stale-context mistakes; assert each arm is kept only if it strictly dominates the arm before it; assert `ab.py` measures and never modifies the live harness. | `ab.py` read-only; never modifies live harness. | The A/B runner (Phase 8) is the only phase that ever *invokes* the current harness — only to measure it, never to modify it. The control plane invents no new model, no new execution substrate, and no new diagnosis path; it reuses the harness's own twenty-two components as the states' bodies and adds only the deterministic workflow control plane and the bounded L slot around them. --- ## 10. Dependencies & Supply-Chain Per Piper's rule: nothing is installed unless >72h old AND (≥10 stars OR deep-scrutinized). This build is **zero-install for Round 1 (Python-only, stdlib + in-repo + reuse of the harness's own stage primitives)**: | Dependency | Why | Status / age-stars | Install needed? | |---|---|---|---| | stdlib `enum` / `typing` | §3.1/§4.2/§4.3/§4.4 the state, transition-kind, gate-operator, and freshness enums; the schemas' type hints | CPython stdlib. | **No** | | stdlib `json` | §4 the StateContract / GatePredicate / Transition / ArtifactFreshness schema serialization | CPython stdlib. | **No** | | stdlib `dataclasses` | §4 the frozen schemas (immutable, rebuilt not mutated) | CPython stdlib. | **No** | | stdlib `collections` / `graphlib` | §4.4 the dependency edges and topological order for recomputation | CPython stdlib. | **No** | | Python toolchain (`python3`, pinned) | §3–§7 all deterministic services | In-repo, pinned interpreter. | **No** | | A model checker (in-repo or a minimal BFS/CTL reachability walker over ≤20 states) | §7 the reachability/safety/liveness queries — a tiny finite graph needs no heavy solver | In-repo, deterministic. | **No** | | Harness components 01–22 (the states' bodies) | §3.1 the states are named phases corresponding to the harness's own stages, reused not duplicated | The harness's own stages, already vetted. | **No** | | Harness weak model (`deepseek-v4-pro`) | §5 the single L entry — the semantic judgment inside a state | The harness's own model, already vetted. | **No** | **Preferred path: zero-install.** Round 1 is Python-only and deterministic: all services use stdlib `enum`/`json`/`dataclasses`/`graphlib`, the model checker is a minimal in-repo reachability walker over a ≤20-state graph, and the states' bodies are **reused from the harness's own components**, not duplicated. **No new package is installed for Round 1.** The DEFERRED rows (§2 rows 9–10) are offline graph tuning (AFlow/GPTSwarm/ADAS/DSPy) and adaptive plan-DAG refinement (CodePlan) — not new third-party Python installs. Any future graph-search library, trained controller, or learned-judgment dependency must clear the **72h-age + star/scrutiny + sandbox-test** gate before use — out of Round 1 scope entirely. --- ## 11. Guardrails & Reversibility **Revocability.** - The build lives entirely in `build/23-workflow-state-machine/`; it never writes into the live harness's source. - A **feature flag** (env var `WORKFLOW=23|free-agent`, default `free-agent` during Round 1 A/B) routes the run; the flag alone switches between the state machine and the free-agent baseline — no code deletion required to revert. The default stays `free-agent` until §8's A/B shows strict domination, because **an empty L column is a permitted, correct state** and an unproven mechanism must not be the default. - `ab.py` is a read-only driver: it *measures* the current harness, never modifies it. Running baseline-vs-arms is always possible in the same session, repo, model. - The workflow ledger (every state entry, every gate evaluation, every tool-boundary event, every freshness invalidation, every retry/rollback/termination traversal, every model-call budget draw) is append-only and versioned; rolling the build back never loses it. This ledger *is* the traceability the paper claims the open floor loses: every state, edge, and artifact dependency is declared, so every decision has a name and an address. **Invariants (must hold, checked at the end of every phase).** 1. **the L column contains at most one entry** — the semantic judgment inside a state (§5), produced only after the deterministic control plane has entered that state, declared its required inputs and output schema, and enforced its tool allowlist; the model never decides *which state is next*, *whether a gate opens*, *which tools it may use*, *whether to retry, roll back, or terminate*, or *whether its output satisfies the schema*. **an empty L column is a permitted, correct state** — a syntax check, a test run, or a freshness recomputation advances the workflow with no model call at all, and the emptiness is the design working, never a violation. 2. **The model never invents a transition** — every edge is declared (§3.1); every gate is harness-executed (§3.2); a cross-state tool call or a traversal of an un-enumerated edge is rejected as `ILLEGAL_TRANSITION`, never honored. 3. **Tool choice is a state property, not a model decision** — the model may call any tool on the state's allowlist and no tool off it; an off-list invocation is `ILLEGAL_TOOL`, rejected at the boundary and never routed. 4. **Staleness propagates downstream only** — a change invalidates and recomputes only affected downstream work; nothing upstream is re-run because something downstream changed; a retry or rollback never invalidates an upstream artifact the failure did not touch. 5. **The graph is model-checked before it runs** — reachability, safety, and liveness (§7) are proven by the deterministic checker on any change to the state registry or transition table; a red query blocks the build. 6. **The controller is tuned offline, never at runtime** — the model never edits its own state machine; any graph change is a design-time, versioned, tested artifact (the DEFERRED rows 9–10), adopted only if it strictly dominates on §8's measures. 7. **All metrics on held-out tasks** — resolve rate, tokens, wall time, LLM calls, illegal/redundant actions, repeated work, regressions, and stale-context mistakes, and every secondary, are reported on held-out tasks, never tuning or in-benchmark data. --- *End of spec. This document is the build contract; the next document records the A/B outcome.*