Disciplines · Audits

Eve SOTA orchestrator model — eve.orchestrator-model.v1

The orchestrator model folds a script of canonical operations into an event stream and then into state, taking every decision through the same exported function the store and the queue use rather than reimplementing any of them.

6sections4 minread
Markdown source
On this page
  • Task: 2.7
  • Evaluated: 2026-09-05
  • Decision: orchestrator-model-and-parity-proof-executable
  • ADR gate: provider-free-model-and-parity-proof (docs/adr/ADR-0076-eve-governed-delivery-lifecycle.md)
  • Record digest: 027fc45ba5bd334b4ef0fadb94216d397bf8795451c6a4bc2d91ce1bcfc8b9e0

The rule#

The orchestrator model folds a script of canonical operations into an event stream and then into state, taking every decision through the same exported function the store and the queue use rather than reimplementing any of them. Both lanes execute one script; ADR-0076’s parity invariant is compared on its own field lists and is proved capable of failing by planted divergences, including a drain that launders an agent’s provenance. Each of the eight fault classes task 2.7 names is asserted as a property that must hold for every schedule of that fault, not as one path that happened to work.

The lane list, the fault vocabulary and all three parity field lists are read from the model; the field lists are then compared to ADR-0076’s own declaration, and each fault and parity claim must name a spec title found in the spec source. The model’s import list is read to confirm every decision is driven rather than copied.

The parity invariant, made executable#

Claim Proved by
equal-over-a-whole-journey "is equal on every field ADR-0076 names, over a whole journey"
catches-an-extra-operation "FAILS when the drain performs an operation the hand lane does not"
catches-laundered-provenance "FAILS when the drain attributes an agent’s report to itself"
orchestration-leaves-no-trace "leaves selection and supervision off the work-item stream entirely"

Compared on 9 folded-state fields and 13 semantic-event fields, normalizing only seq, createdAt, conversationRef — each list read from the model and then checked against ADR-0076's own declaration, so a proof cannot quietly compare less than the invariant claims.

The eight fault classes#

Fault Proved by
duplicate delivery "a redelivered keyed request appends NOTHING, in either lane"
lease expiry/renewal races "a renewal that arrives after expiry is refused, not silently granted"
stale fencing "a write carrying a superseded token is refused even from the same agent"
crash between side effect and report "the ledger shows the work unreported rather than inventing the report"
dependency cycles "an item in a declared cycle is never acquired, in either lane"
poison items "the retry budget is spent in acquisitions and stops the cycle"
cancellation "stopping between items leaves the finished ones whole and starts nothing new"
restart from persisted state "replaying the persisted events recovers exactly the state that was lost"

Decisions driven, never copied#

  • replayLedger from intent-store.js
  • checkTransition from intent-machines.js
  • WORK_ITEM_GRAPH from intent-machines.js
  • admitLease from queue-semantics.js
  • checkFence from queue-semantics.js
  • checkRenewal from queue-semantics.js
  • resolveIdempotency from queue-semantics.js
  • stepQueueState from queue-semantics.js
  • triageRequiredFor from triage.js

Rigour#

  • An operation the model does not know throws rather than being skipped: true
  • The parity proof is shown capable of failing: true
  • Actor provenance is never normalized away: true
  • Refusals are compared, not just surviving events: true
  • The lane never reaches a decision: true
  • The model reads no clock: true

Honest limits#

  • This record closes task 2.7 only. It does not drain a real backlog or run a soak; task 2.8 owns both, and only after the Security, Evaluation and Reliability gates admit them.
  • The model is provider-free by construction, which is its strength and its boundary: it proves what the decision functions do with the inputs it constructs, not what PostgreSQL does under concurrent writers. The real-database behaviour of those same decisions is covered by the integration specs from tasks 2.2 and 2.4.
  • Parity is proved over scripts this suite writes. It is a property over those schedules rather than an exhaustive search: a divergence reachable only by an operation ordering nothing here constructs would not be found.
  • The fault cases model each fault as the shape the plane actually sees — a redelivery as a repeated keyed request, a crash as a stream that simply stops, a cancellation as a prefix. They do not kill processes or sever sockets; the drain tests and the end-to-end probe from tasks 2.3 and 2.6 do that.
  • The lane distinction is modelled at the level of who issues which operation and what orchestration is recorded beside it. A real drain additionally spawns and supervises a process, and that half is proved by the drain tests rather than here.
  • The model drives the decisions the store exports. A decision the store makes INSIDE a transaction that it does not export — an ordering the database enforces, say — is outside what a provider-free model can reach.