Stateful Workflow Execution

Table of contents

Stateful Workflow Execution

A regulated composition: a multi-actor gated workflow made auditably complete. A Workflow / State Machine instance governs the overall process lifecycle (declared states and transitions); specific declared transitions are gated by human Approval Steps bound at the composition layer; Permissions governs who may start a workflow and fire transitions; Assignment puts each open gate in the right approver’s in-tray; and Audit Trail (as regulated-audit substrate) makes every transition and every gate decision attributed, retention-bounded, tamper-sealed, and reconstructible from the records alone. The headline emergent property: guard evaluation re-converges here. Workflow / State Machine deliberately does not evaluate guards (it trusts a caller-asserted guard_satisfied); this composition evaluates approval-type guards by binding each guarded transition to an Approval Step and firing the transition only when that step is in Approved — closing the exact gap Workflow / State Machine left open.

Intent

Multi-step regulated processes share a common structure: an entity moves through a declared sequence of states, some transitions require explicit human approval before they may fire, every transition must be attributed and tamper-evidenced, and the entire history must be reconstructible from the records alone. A pharmaceutical batch-release process requires declared quality-control steps with a qualified-person approval gate before release. A financial journal-entry promotion requires controller sign-off at the booking gate. A clinical-trial protocol change requires investigator and sponsor approvals before the change may proceed. A software change request requires a review approval before it can be merged to production. In every case the structure is the same: a declared state machine governing the process instance, a set of gates (transitions that may not fire until a named approver has actually decided), an authorization surface governing who may advance the process at all, a work-tracking surface that keeps each pending gate in the right person’s in-tray, and a regulated-audit substrate that makes every advancement and every gate decision attributed, sealed, and retention-governed.

The constituent atoms address each of these concepts freestanding. Workflow / State Machine enforces declared-transition discipline — only declared transitions fire, exactly one current state at all times, the full transition history is append-only, total-ordered, and replay-deterministic. Approval Step is the per-gate primitive — one named approver, one subject, one scope, one outcome (Pending → Approved Rejected Withdrawn), with approver exclusivity enforced by its Invariant 4. Permissions governs standing authorization — who holds the workflows:start and workflows:fire grants that permit process-level actions. Assignment binds each open gate to the named approver’s in-tray and recalls the binding when the gate is decided. Audit Trail is the regulated-audit substrate that supplies Event Log, Actor Identity, Retention Window, and Tamper Evidence as a single composition.

What the constituent atoms cannot answer alone is the central regulated question: did this guarded transition fire only after its named approval was genuinely recorded? Workflow / State Machine’s guard model (Invariant 8 — guard-gating without evaluation) deliberately does not evaluate guard predicates; it trusts a caller-asserted guard_satisfied = true and records the assertion. Its Edge cases name this as a calling-system obligation and explicitly flag approval-gate evaluation as the concept this composition (Stateful Workflow Execution, C10) re-converges. This composition is where that re-convergence happens: it binds each guarded transition to an Approval Step (gate_binding), reads the bound step’s state before any fire call, and asserts guard_satisfied = true to WorkflowStateMachine.fire only when the bound step is in Approved. The caller of this composition never supplies guard_satisfied directly for a guarded transition; the composition derives it from the gate’s actual approval record.

This is not a new primitive. The five constituent atoms (and the Audit Trail substrate) are unchanged. The composition is the wiring that makes their concepts coherent — one consolidated multi-actor regulated-workflow surface rather than five parallel record stores the auditor must correlate by hand.

The composition addresses what Workflow / State Machine’s EOS (Essence of Software — Daniel Jackson’s framework for specifying software concepts as freestanding, composable units) extraction correctly deferred: guard evaluation, non-repudiable attribution, retention governance, Permissions gating, and the in-tray binding for pending approvals. The composition resolves those deferred obligations without re-deriving the underlying primitives.

Summary

Stateful Workflow Execution wires five building blocks together into a single regulated workflow surface. The process map — which states exist, which transitions between them are allowed, which transitions require a human approval before they can fire — is declared once at the start and frozen for the lifetime of that process instance. A Permission system controls who may start a workflow or advance it. For transitions that require approval, the composition opens a gate (an Approval Step bound to the transition) and puts it in the named approver’s work-queue (an Assignment); the transition cannot fire until the approver actually approves. A tamper-evident audit record (the Audit Trail substrate) stamps and seals every transition and every gate decision with the acting actor’s identity, retention-governs the record, and provides the forensic foundation for a records-alone process proof. These guarantees together produce what none of the building blocks can provide alone: a regulated proof that the process moved only through its declared transitions, that every gated transition had a real human approval behind it (not just a bare assertion), and that the complete history is attributed, sealed, and reconstructible. This composition is the structural form of FDA (US Food and Drug Administration) 21 CFR (Code of Federal Regulations) Part 11 electronic records workflows, SOX (Sarbanes-Oxley Act — US law on corporate financial reporting and records integrity) §404 process-control records, ISO (International Organization for Standardization) 9001 §8.5.1 production-process documentation, and any other regulated domain where the question “prove that this process followed its declared path and that each gate was genuinely cleared” must be answered from records alone.

Composes

Workflow / State Machine — the orchestrating spine. Provides the declared-state-machine enforcement: only declared transitions fire; exactly one current state at all times; the full transition history is append-only, total-ordered by sequence number, and replay-deterministic. The composition instantiates one Workflow / State Machine instance per workflow run, supplies it the deployment-declared process declaration, and calls fire on it as the sole write path — the composition never bypasses fire.

Approval Step — the per-gate human-approval primitive. Provides the gate record: one Approval Step per guarded transition that becomes relevant, each carrying its own step_id, subject_ref, approver_ref, submitter_ref, scope, lifecycle (Pending → Approved Rejected Withdrawn), and Invariant 4 enforcement that only the named approver_ref may transition to Approved or Rejected. The composition submits one Approval Step when a gate is opened, reads its state when the corresponding transition is to be fired, and supplies guard_satisfied = true to WorkflowStateMachine.fire only when the step is in Approved.

Permissions — the authorization surface for workflow-level actions. Provides grant, revoke, and permitted. Every workflow-level state-changing action (start_workflow, fire_transition) and every workflow-level read query (read_workflow) is gated by a permitted check before reaching any constituent store. Step-level gate decisions (decide_gate) are enforced by Approval Step’s Invariant 4 (named-approver exclusivity) directly — no redundant chain-layer permission check, mirroring Multi-Party Approval’s scope-vocabulary discipline.
Assignment — the in-tray binding for open gates. On gate opening, one Assignment record is created (task_ref = step_id, assignee_ref = approver_ref from the gate_spec) so the named approver can query “which approval gates are currently in my in-tray?” via Assignment’s query surface. When the gate is decided (Approved, Rejected, or Withdrawn), the corresponding Assignment is recalled — the responsibility is discharged.
Audit Trail — the regulated-audit substrate. Every workflow-level action (workflow_started, gate_opened, gate_decided, transition_fired) is recorded as one record_action call on the Audit Trail instance, producing an Event Log entry, an Actor Identity attestation, a Retention Window record, and (per the deployment’s seal cadence) a Tamper Evidence seal. The composition maintains exactly one Audit Trail instance configured with the deployment’s regulatory retention policy. The Event Log and Actor Identity atoms that the roadmap entry for this composition listed as prerequisites are reached transitively through Audit Trail; the composition does not maintain separate Event Log or Actor Identity instances.

Composition logic

Composition state

The composition owns emergent state — the workflow store, the gate binding maps, and the cross-atom traversal maps — that wires the constituent atoms into one queryable regulated-workflow surface. None of these state elements belongs to any single constituent atom.

workflow_store — the set of workflow instance records. Each record carries: instance_id (the Workflow / State Machine instance id, assigned by the constituent at start_workflow), subject_ref (an opaque reference to the entity whose lifecycle this workflow governs), initiator_ref (the actor who started the workflow), declaration_ref (an opaque reference identifying the deployment’s declared process definition — the exact declaration supplied at start_workflow), gate_spec (the map from each guarded transition’s guard label to {approver_ref, scope} naming the approval required for that gate; set at start_workflow, immutable), and started_at. The workflow record is immutable on every field from the moment start_workflow returns; the Workflow / State Machine constituent owns current_state and the transition history.
gate_binding — map from (instance_id, guarded transition action name) to the step_id of the Approval Step that gates it. Set when open_gate opens a gate for a given (instance_id, action) pair. This is the load-bearing traversal from a guarded transition to its approval record: at fire_transition, the composition reads gate_binding[(instance_id, action)] to find the step, then reads the step’s state to determine whether guard_satisfied may be asserted. Keys are immutable from the moment open_gate returns for a given pair; no re-binding of a guarded transition to a different step under the same (instance_id, action) pair is permitted in the same workflow instance.
gate_to_assignment — map from step_id (a gate’s Approval Step id) to the assignment_id of its in-tray binding. Set when open_gate creates the Assignment. Used at decide_gate to recall the in-tray binding when the gate is decided, and during moot-gate cascade when the workflow leaves a transition’s from_state by firing a different transition out of it.
transition_to_event — map from a fired transition’s transition_id (the Workflow / State Machine history entry id) to the Audit Trail event_id that attributes and seals the firing. Set at fire_transition after WorkflowStateMachine.fire succeeds and AuditTrail.record_action returns an event_id. The traversal backbone for the forensic query: from a transition in the Workflow / State Machine history to its Audit Trail attestation.

Configuration

audit_trail_retention_policy — the policy reference passed to the Audit Trail instance at each record_action call. Typically a regulatory policy id (sox_7_year, fda_part_11_predicate_rule, hipaa_6_year, ich_e6_tmf). The choice is deployment policy; the composition surfaces the configuration knob but does not enforce a default. Regulated deployments must configure this explicitly; a deployment silent on retention policy accepts the Audit Trail instance’s own default, which is a deployment-policy choice the composition cannot evaluate.
application_actor_ref and application_credential — the deployment-provisioned actor reference and credential the composition uses when emitting composition-internal Audit Trail entries that have no direct human-actor origin: specifically, the moot_gate_recalled event produced when the composition cascade-recalls a gate that has become unreachable because the workflow left its from_state by firing a different transition. The composition actor is a first-class registered actor in the Audit Trail’s underlying Actor Identity registry — not a special-cased nil — and its attestations verify under the same rules as human-actor attestations. The deployment is responsible for issuing, rotating, and retiring this credential under the same Permissions and operational discipline applied to any privileged service identity. An auditor querying the Audit Trail sees moot_gate_recalled events attributed to the composition actor and can verify them against the registry’s public material exactly as for human-actor events. The forgery defense for composition-actor events rests on the composition’s own structural records: a forged moot_gate_recalled event claiming a gate was recalled for a transition that the Workflow / State Machine history shows was actually fired (rather than superseded by an alternate transition) is detectable by cross-referencing the event against the transition history. The distinguishing rule: moot_gate_recalled is the sole event emitted with actor_ref = application_actor_ref; all other workflow events use the human actor’s reference.

Scope vocabulary

Permissions treats action scopes as opaque. Stateful Workflow Execution defines the canonical scope vocabulary for its Permissions instance:

Scope	Permits
`workflows:start`	Call `start_workflow` to instantiate a new workflow run
`workflows:open-gate`	Call `open_gate` to open an approval gate for a guarded transition
`workflows:fire`	Call `fire_transition` to advance the workflow through a transition
`workflows:read`	Read workflow records and their composed gate, assignment, and attestation surface

Gate decisions (decide_gate, which wraps Approval Step’s approve/reject/withdraw) are not additionally permission-gated at the workflow layer: Approval Step’s Invariant 4 (only the named approver_ref may transition Pending to Approved or Rejected) and Invariant 5 (only the named submitter_ref may transition Pending to Withdrawn) are the structural enforcement for who may decide each gate. Adding a second permission check at the workflow layer would be redundant and risks the two checks drifting out of sync. The workflow composition relies on Approval Step’s enforcement and surfaces an unauthorized rejection from the underlying atom unchanged, mirroring Multi-Party Approval’s scope-vocabulary discipline.

The vocabulary is deployment-configurable. A deployment that distinguishes initiator roles (e.g., workflows:start:pharma-batch, workflows:start:financial-journal) introduces finer-grained scopes and adjusts the wiring accordingly; the canonical vocabulary above is the minimum useful set.

Primitive policies

These input-validation rules apply at the composition boundary before any constituent atom is invoked. They close the “but what does X mean exactly?” class of Pass 3 findings up front.

actor_ref, subject_ref, initiator_ref, approver_ref, submitter_ref — must each contain at least one non-whitespace character. Null, empty, or whitespace-only values are invalid-request at the composition boundary before any Permissions or constituent call.
credential — must be a parseable, non-null value of the deployment’s declared credential type. Malformed credentials are invalid-request before any constituent call.
reason — optional on start_workflow, open_gate, fire_transition. Required as the reason argument passed into decide_gate for gate decisions of type Rejected or Withdrawn (propagated from Approval Step’s reject/withdraw mandatory-reason rule). If supplied in any action, must contain at least one non-whitespace character.
gate_spec — at start_workflow, the composition validates that gate_spec covers exactly the set of guarded transitions in the supplied declaration: for every transition in the declaration carrying a guard label, gate_spec must contain an entry keyed by that guard label, and each entry must carry a non-whitespace approver_ref and a non-whitespace scope. A gate_spec with entries for guard labels not present in the declaration is invalid-request (the deployment named a gate that will never be used). A declaration with guarded transitions for which gate_spec has no entry is invalid-request (a guarded transition with no named approver cannot be governed). The gate_spec validation is part of start_workflow step 2; no WorkflowStateMachine.instantiate call is made until gate_spec passes.
instance_id — must contain at least one non-whitespace character for all actions that take it. Non-whitespace enforcement follows Workflow / State Machine’s own instance_id rule.
decision — at decide_gate, must be one of the string literals "approve", "reject", or "withdraw"; any other value is invalid-request.

Action wiring

Every workflow-level action follows the same three-step shape: Permissions check first, constituent atom call(s) second, Audit Trail record third. Gate-decision actions delegate structural authorization to Approval Step and record second. Each action lists the full rejection taxonomy; every constituent rejection is either propagated, renamed, or surfaced as a new code at the composition boundary.

`start_workflow(actor_ref, declaration, subject_ref, gate_spec, credential, [reason]) → {instance_id} | rejected(permission-denied | invalid-declaration | invalid-request | recording-failure)`

Permissions.permitted(actor_ref, workflows:start) → if denied, return rejected(permission-denied).
Validate gate_spec against declaration per Primitive policies: every guarded transition in the declaration has a matching entry in gate_spec; every gate_spec entry names a real guard label; every entry carries non-whitespace approver_ref and scope. Validate subject_ref per Primitive policies (non-whitespace). Any violation is rejected(invalid-request). No Workflow / State Machine call is made until this passes.
Call WorkflowStateMachine.instantiate(declaration, actor_ref, instance_metadata={subject_ref, gate_spec_labels}, instantiated_at=now) → instance_id | rejected(invalid-declaration). Propagate invalid-declaration unchanged. storage-failure from the constituent surfaces as recording-failure.
Write the workflow_store record: {instance_id, subject_ref, initiator_ref=actor_ref, gate_spec, started_at=now}. storage-failure here is recording-failure.
Call AuditTrail.record_action(action_ref=workflow_started, actor_ref, credential, data={instance_id, subject_ref, gate_spec_labels, reason?}, retention_policy=audit_trail_retention_policy) → event_id | rejected(...). Any Audit Trail failure surfaces as recording-failure. (Note: gates are opened lazily — see open_gate — not at start. The started_at record and the Audit Trail event together prove the workflow began and under which actor’s authority.)
Return {instance_id}.

Partial-failure recovery. If step 3 succeeds but step 4 or step 5 fails, the Workflow / State Machine instance exists in its constituent store but the composition’s workflow_store has no record. The recovery path: the composition does not issue the instance_id to the caller and surfaces recording-failure; the orphaned Workflow / State Machine instance is quarantined (it will never be referenced by this composition’s workflow_store) and may be cleaned up by the deployment’s store-maintenance process. The caller must retry start_workflow from scratch, producing a new instance_id.

`open_gate(actor_ref, instance_id, action, credential) → {step_id, assignment_id} | rejected(permission-denied | not-known | invalid-transition | not-guarded | gate-not-available | already-open | recording-failure)`

This action opens an approval gate for a guarded transition whose from_state equals the workflow instance’s current state. Gates are opened lazily — the composition does not open all gates at start, only when the workflow has reached the state from which the guarded transition departs and an actor with workflows:open-gate authority decides to open it.

Permissions.permitted(actor_ref, workflows:open-gate) → if denied, return rejected(permission-denied).
Look up workflow_store[instance_id] → not-known if absent.
Call WorkflowStateMachine.read_declaration(instance_id) to retrieve the immutable declaration. Identify the declared transition matching (current_state, action): call WorkflowStateMachine.current(instance_id) → current_state. If no declared transition has (from_state = current_state, action = action), return invalid-transition. If the matched transition has no guard label, return not-guarded (unguarded transitions are fired directly without opening a gate).
Check gate-not-available: if current_state ≠ the matched transition’s from_state the check is definitionally satisfied by step 3 (we derived current_state there); the secondary case is that the workflow is in a terminal state — WorkflowStateMachine.fire would return terminal — confirmed by checking whether current_state ∈ terminal_states in the declaration. If terminal, return gate-not-available (a terminal instance cannot have gates opened).
Check already-open: if gate_binding[(instance_id, action)] already exists, return already-open (a gate is already bound for this (instance_id, action) pair; call decide_gate to resolve the existing gate before opening a replacement).
Call ApprovalStep.submit(subject_ref=workflow_store[instance_id].subject_ref + ":" + action, approver_ref=gate_spec[guard_label].approver_ref, submitter_ref=workflow_store[instance_id].initiator_ref, scope=gate_spec[guard_label].scope) → step_id | rejected(invalid-request | storage-failure). Propagate failures as recording-failure. The gate’s submitter_ref is the workflow’s initiator_ref, not the open_gate caller — so the withdrawal authority over the gate (Approval Step Invariant 5: only the submitter may withdraw) belongs to the workflow initiator, which is what makes both decide_gate(withdraw) and the composition’s moot-gate cascade (which withdraw with withdrawn_by = initiator_ref) authorized. The open_gate caller is recorded as the actor on the gate_opened Audit Trail event (step 9), preserving the attribution of who opened the gate; the withdrawal authority is the initiator’s, mirroring Multi-Party Approval’s initiator-owns-withdrawal discipline.
Call Assignment.assign(task_ref=step_id, assignee_ref=gate_spec[guard_label].approver_ref) → assignment_id | rejected(...). Propagate failures as recording-failure.
Write: gate_binding[(instance_id, action)] = step_id; gate_to_assignment[step_id] = assignment_id. storage-failure is recording-failure.
Call AuditTrail.record_action(action_ref=gate_opened, actor_ref, credential, data={instance_id, action, step_id, assignment_id, approver_ref, scope}, retention_policy=audit_trail_retention_policy). Failure is recording-failure.
Return {step_id, assignment_id}.

Partial-failure recovery. If step 6 or 7 succeeds but subsequent writes fail: the composition surfaces recording-failure; the orphaned Approval Step or Assignment must be withdrawn/recalled by the deployment’s store-maintenance process before retry. A partial gate_binding write (step 8 fails) leaves no binding in the composition’s emergent state; the constituent records are present but un-traversable from the composition layer. Recovery: clean the orphan constituent records and retry open_gate.

`decide_gate(actor_ref, instance_id, action, decision, reason, credential) → approved | rejected_outcome | withdrawn | rejected(not-known | gate-not-open | not-pending | unauthorized | invalid-request | recording-failure)`

This action wraps the Approval Step’s approve/reject/withdraw on the bound gate for (instance_id, action). Structural authorization (only the named approver_ref may approve or reject; only submitter_ref may withdraw) is enforced by Approval Step’s Invariant 4 and Invariant 5 directly; no redundant Permissions check is added.

Look up workflow_store[instance_id] → not-known if absent.
Look up gate_binding[(instance_id, action)] → step_id. If no binding exists, return gate-not-open (there is no Approval Step open for this transition; call open_gate first).
Validate decision is one of {"approve", "reject", "withdraw"} → invalid-request otherwise.
Dispatch on decision:
- "approve": call ApprovalStep.approve(step_id, decided_by=actor_ref, reason?, decided_at=now) → approved | rejected(invalid-request | not-known | not-pending | unauthorized | storage-failure). Propagate not-pending and unauthorized unchanged; map storage-failure to recording-failure.
- "reject": call ApprovalStep.reject(step_id, decided_by=actor_ref, reason, decided_at=now) → rejected_outcome | rejected(...). reason is required; a null or whitespace-only reason is caught at the Primitive policies layer and returned as invalid-request before this call is made. Propagate rejections as above.
- "withdraw": call ApprovalStep.withdraw(step_id, withdrawn_by=actor_ref, reason, withdrawn_at=now) → withdrawn | rejected(...). reason is required. Gate withdrawal is the workflow initiator’s act: because the gate’s Approval Step carries submitter_ref = initiator_ref (set at open_gate step 6), Approval Step Invariant 5 admits a withdrawal only when actor_ref is the workflow initiator; a non-initiator withdrawal attempt surfaces unauthorized unchanged. Propagate rejections as above.
On atom-level success, recall the in-tray binding: Assignment.recall(gate_to_assignment[step_id]). If the assignment is already in Recalled state (idempotent recall — a moot-gate cascade has already discharged it), treat not-active as no-op success.
Call AuditTrail.record_action(action_ref=gate_decided, actor_ref, credential, data={instance_id, action, step_id, decision, reason?}, retention_policy=audit_trail_retention_policy). Failure is recording-failure. If this record_action fails after the Approval Step transition succeeded, the recovery path in Edge cases Cross-store consistency under failure applies.
Return the outcome token from step 4 (approved, rejected_outcome, or withdrawn).

`fire_transition(actor_ref, instance_id, action, credential) → new_state | rejected(permission-denied | not-known | terminal | invalid-transition | gate-not-cleared | recording-failure)`

This is the composition’s load-bearing wiring action. For unguarded transitions, it calls WorkflowStateMachine.fire directly. For guarded transitions, it reads the bound gate’s Approval Step state and asserts guard_satisfied = true only when the step is in Approved.

Permissions.permitted(actor_ref, workflows:fire) → if denied, return rejected(permission-denied).
Look up workflow_store[instance_id] → not-known if absent.
Call WorkflowStateMachine.read_declaration(instance_id) and WorkflowStateMachine.current(instance_id) to determine the matched transition and whether it is guarded. If no declared transition matches (current_state, action), WorkflowStateMachine.fire would return invalid-transition; return invalid-transition. If current_state ∈ terminal_states, return terminal.
For an unguarded transition (the matched transition has no guard label): a. Call WorkflowStateMachine.fire(instance_id, action, actor_ref, fired_at=now) → new_state | rejected(...). Propagate constituent rejections: not-known → not-known; terminal → terminal; invalid-transition → invalid-transition; storage-failure → recording-failure. (The guard-not-satisfied rejection from the constituent is not reachable here because the transition is unguarded and the composition does not pass guard_satisfied.) b. On constituent success, write transition_to_event at step 4c below.
For a guarded transition (the matched transition carries a guard label): a. Look up gate_binding[(instance_id, action)] to find the bound step_id. If no binding exists, the gate has not been opened — the composition refuses to fire: return gate-not-cleared (the guarded transition cannot be asserted until its gate is opened and resolved). b. Read the Approval Step state for step_id via ApprovalStep.read({step_id}). If the step is not in Approved state, return gate-not-cleared. The composition evaluates the guard by reading the gate state; it does not delegate this check to the caller. A gate in Pending, Rejected, or Withdrawn state prevents the guarded transition from firing. The caller cannot override this: there is no surface by which the caller supplies guard_satisfied for a guarded transition in this composition. c. The step is in Approved. Call WorkflowStateMachine.fire(instance_id, action, actor_ref, guard_satisfied=true, fired_at=now) → new_state | rejected(...). The composition asserts guard_satisfied = true here because it has just verified, from the bound Approval Step’s actual state, that the named approver approved. Propagate constituent rejections as in step 4a. d. On constituent success, proceed to step 4b (writing transition_to_event).
On constituent fire success (either path): call AuditTrail.record_action(action_ref=transition_fired, actor_ref, credential, data={instance_id, action, from_state=prior current_state, new_state, transition_id, guarded=<bool>, step_id if guarded}, retention_policy=audit_trail_retention_policy) → event_id. Write transition_to_event[transition_id] = event_id. Failure is recording-failure. If record_action fails after WorkflowStateMachine.fire succeeded, see Cross-store consistency under failure in Edge cases; the composition surfaces recording-failure but the Workflow / State Machine transition has committed.
Moot-gate cascade: after a successful fire_transition, check whether the workflow’s new current_state is different from the from_state of any currently open gate (i.e., gate_binding entries for this instance_id whose associated Approval Step is still in Pending and whose declared transition’s from_state ≠ new_state). Any such gate is now moot — the workflow has left the state from which that guarded transition departs, so the gate will not be evaluated unless the workflow returns to that state (which is only possible if the declaration includes a return path, per the Workflow / State Machine’s declared-transition model). For each moot gate identified:
- Call ApprovalStep.withdraw(step_id, withdrawn_by=initiator_ref, reason="Gate moot: workflow left the gate's from_state by firing a different transition") → if not-pending, the gate was already decided — no action needed.
- Call Assignment.recall(gate_to_assignment[step_id]) → treat not-active as idempotent success.
- Call AuditTrail.record_action(action_ref=moot_gate_recalled, actor_ref=application_actor_ref, credential=application_credential, data={instance_id, moot_action=action, step_id, reason="Gate moot: workflow advanced past from_state"}, retention_policy=audit_trail_retention_policy).
- Remove gate_binding[(instance_id, moot_action)] and gate_to_assignment[step_id] from the composition’s maps.
Return new_state.

`read_workflow(actor_ref, query) → workflow_view | rejected(permission-denied | invalid-query)`

Permissions.permitted(actor_ref, workflows:read) → if denied, return rejected(permission-denied) (or an empty result, per deployment policy).
Query workflow_store on the supported filter axes: instance_id, subject_ref, initiator_ref, started_at range (using {after: <timestamp>, before: <timestamp>} sub-key form). An unrecognized filter key is invalid-query. An empty result for a well-formed query is an empty list, not a rejection.
For each workflow instance in the result set, the response carries a composed view: the workflow record fields (instance_id, subject_ref, initiator_ref, declaration_ref, gate_spec, started_at); the Workflow / State Machine’s current_state and transition_history (via WorkflowStateMachine.current and WorkflowStateMachine.history); the full transition history enriched with each transition’s Audit Trail event_id (via transition_to_event); and each gate’s Approval Step record (via gate_binding joined against the Approval Step store) with its Assignment status (via gate_to_assignment joined against the Assignment store). The composition does not surface the underlying Audit Trail event payloads on this query; auditors querying the full audit evidence call AuditTrail.verify_record directly with the relevant event_ids.

The load-bearing wiring decision — approval-gated transition (guard evaluation via Approval Step)

Principle. A regulated multi-actor workflow requires that a guarded transition cannot fire until its named human approval is genuinely recorded (attributed, sealed, and retention-governed) and that the process moved only through declared transitions. These two properties together constitute a records-alone-provable gated process.

Likely objection. “Workflow / State Machine already has a guard-gating mechanism — it accepts guard_satisfied = true from the caller. Why not let the caller assert it, or let the composition simply trust the caller’s word?”

Mechanism that resolves it. Workflow / State Machine deliberately extracted guard evaluation as an EOS boundary (its Edge cases explicitly name this composition as the re-convergence point): guards recur across many forms — approval records, threshold evaluations, quorum counts, external conditions — and each has its own state machine. The atom correctly does not absorb any of them. For approval-type guards, this composition is the designated evaluation layer. The mechanism: the composition binds each guarded transition to an Approval Step (gate_binding) at gate-opening time, and at fire_transition reads the bound step’s actual state. guard_satisfied = true is asserted to WorkflowStateMachine.fire if and only if the bound step is in Approved. The caller of this composition supplies no guard_satisfied argument; the composition’s own read of the Approval Step state is the evaluation. The gate is structurally closed: an actor with workflows:fire and a guarded transition they want to advance cannot assert the guard themselves — the approval record must exist.

Result. A records-alone-provable gated workflow: the process moved only through declared transitions (Workflow / State Machine Invariants 3 and 8, preserved by the composition); each guarded transition cleared its named approval by the authorized actor (Approval Step Invariant 4, enforced at gate-decision time, verified by the composition at fire time); all transition firings and all gate decisions are attributed, sealed, and retention-governed (Audit Trail substrate). An auditor reconstructing the process from the records alone sees: every transition is declared; every guarded transition’s history entry corresponds to a bound Approval Step in Approved state; every action is attributed to a real registered actor under Actor Identity attestation. No transition fired on a bare caller assertion.

Composition-level invariants

These invariants (conditions that must always hold) emerge from the composition. None belongs to a single constituent atom; each requires two or more constituents working together to hold. Each invariant names the constituent invariants it depends on and the action wiring step that establishes it.

Invariant 1 — Approval-gated transition (load-bearing). A guarded transition’s history entry exists in the Workflow / State Machine instance only if its bound Approval Step (via gate_binding[(instance_id, action)]) is in Approved state at the moment fire_transition called WorkflowStateMachine.fire with guard_satisfied = true. The composition evaluates the gate (reads the Approval Step state at fire_transition step 5b) and asserts guard_satisfied = true only on a confirmed Approved step; a guarded transition never fires on a bare caller assertion. Rests on Workflow / State Machine Invariants 3 (only-declared-transitions) and 8 (guard-gating without evaluation) plus Approval Step Invariant 4 (approver exclusivity). This invariant is the composition’s foundational record-alone-provable claim: a history entry with guard_satisfied = true means the composition verified an Approved gate, not merely trusted a caller.
Invariant 2 — Permission-gated process advancement. No transition fires by an actor lacking workflows:fire; no workflow is started by an actor lacking workflows:start; no gate is opened by an actor lacking workflows:open-gate. Gate decisions are enforced by Approval Step Invariants 4 and 5 (named-approver exclusivity and submitter exclusivity) directly — no redundant chain-layer Permissions check for gate decisions. Rests on fire_transition step 1, start_workflow step 1, and open_gate step 1 Permissions checks, plus Approval Step Invariants 4 and 5.
Invariant 3 — Attributed and sealed history. Every fired transition (both guarded and unguarded) and every gate decision (opened, decided) and every workflow start produces exactly one AuditTrail.record_action call, each returning an event_id. The full workflow and gate lifecycle is reconstructible forward via Audit Trail (ordered by the Audit Trail’s sequence) and reverse via the workflow records (via transition_to_event and gate_binding). Inherits Audit Trail’s atomicity surface: record_action is treated as atomic from this composition’s perspective, modulo Audit Trail’s own Partial attestation on step failure edge case (Actor Identity.attest succeeds but EventLog.append fails), whose recovery is inherited from the substrate and not re-derived here. Rests on start_workflow step 5, open_gate step 9, decide_gate step 6, fire_transition step 6, and the Audit Trail substrate’s composition-level invariants.
Invariant 4 — Gate assignment coverage and moot-gate cascade. Every open gate (a submitted, undecided Approval Step bound via gate_binding to a transition reachable from the current state) has exactly one Active Assignment with task_ref = step_id and assignee_ref = approver_ref from the gate_spec. Assignments are recalled in two cases: (a) when the gate is decided (decide_gate step 5), the Assignment is recalled in the same composition-level action; (b) when the workflow fires a transition that leaves the gate’s from_state by an alternate path (moot-gate cascade in fire_transition step 7), every still-Active Assignment for moot gates is recalled and the bound Approval Steps are withdrawn. After either case, no gate has a lingering Active Assignment. An ApprovalStep.withdraw that returns not-pending (the gate was already decided) and an Assignment.recall that returns not-active (the binding was already discharged) are treated as idempotent no-op successes. Rests on open_gate steps 7–8, decide_gate step 5, and fire_transition step 7.
Invariant 5 — Only-declared-transitions and replay determinism preserved. The composition never bypasses WorkflowStateMachine.fire; every transition in the Workflow / State Machine history is a declared transition; current_state replays deterministically from the history. This is the constituent invariant of Workflow / State Machine (Invariants 3, 7) preserved and surfaced at the composition level because it is load-bearing for the audit proof. The composition adds no alternate write path to the Workflow / State Machine’s transition history. Guarded transitions fire through the same fire surface as unguarded transitions; the only difference is whether guard_satisfied is asserted (and if so, the composition asserts it, not the caller).
Invariant 6 — Records-alone process proof (forensic completability). read_workflow (combined with AuditTrail.verify_record on the event_ids from transition_to_event) lets an auditor prove from the records alone: (a) the process moved only through declared transitions; (b) each guarded transition’s history entry corresponds to a bound Approval Step in Approved state (via gate_binding); (c) the approving actor on the Approval Step matched approver_ref from the gate_spec (Approval Step Invariant 4); (d) the workflows:fire grant was held by the actor who fired each transition (Audit Trail Actor Identity attestation); (e) the complete history is attributed and sealed. This is the emergent guarantee no single constituent provides: Workflow / State Machine provides (a); Approval Step provides (b) and (c); Permissions provides (d); Audit Trail provides attribution and sealing for the combined record. The composition provides all five in one queryable surface.
Invariant 7 — Constituent invariants preserved. All invariants of every constituent atom hold over its respective instance. Workflow / State Machine’s invariants (declaration immutability, exactly one current state, only-declared-transitions, terminal absorption, history append-only and complete, history total order, replay determinism, guard-gating without evaluation, transition attribution completeness, instance store durability) hold per workflow instance. Approval Step’s invariants hold per gate step. Permissions’ invariants hold over the workflow-store-scoped Permissions instance. Assignment’s invariants hold over the composition’s Assignment instance. Audit Trail’s composition-level invariants hold over its instance.

Examples

Walkthrough — FDA 21 CFR Part 11 / ISO 9001 pharmaceutical batch release

A pharmaceutical manufacturer’s batch-release system uses Stateful Workflow Execution to govern the lifecycle of batch BR-2026-0412 under FDA 21 CFR Part 211 (Current Good Manufacturing Practice for Finished Pharmaceuticals) and FDA 21 CFR Part 11 (Electronic Records; Electronic Signatures). The deployment configures audit_trail_retention_policy = fda_part_11_predicate_rule.

Declaration. The deployment declares the following process:

states: {sampled, testing, qp-review, released, rejected}
transitions: [
  {from: sampled,    action: begin-testing,  to: testing},
  {from: testing,    action: complete-tests, to: qp-review},
  {from: qp-review,  action: release,        to: released, guard: "QP-sign-off"},
  {from: qp-review,  action: reject-batch,   to: rejected, guard: "QP-rejection"},
  {from: testing,    action: fail-tests,     to: rejected}
]
initial_state: sampled
terminal_states: {released, rejected}

The gate_spec maps "QP-sign-off" to {approver_ref: "qp_director_santos", scope: "pharma:batch-release:qp-sign-off"} and "QP-rejection" to {approver_ref: "qp_director_santos", scope: "pharma:batch-release:qp-rejection"}.

QA manager starts the workflow. start_workflow(actor_ref=qa_manager, declaration, subject_ref="br-2026-0412", gate_spec, credential=qa_credential) → Permissions returns permitted (qa_manager holds workflows:start); gate_spec validates (two guarded transitions, two matching entries); WorkflowStateMachine.instantiate(declaration) → instance_id="wf-batch-br-2026-0412"; workflow_store record written; Audit Trail records workflow_started. Returns {instance_id="wf-batch-br-2026-0412"}.
Lab technician begins testing. fire_transition(actor_ref=lab_tech_rivera, instance_id, action="begin-testing", credential) → Permissions permitted; begin-testing is an unguarded transition; WorkflowStateMachine.fire(instance_id, "begin-testing", actor_ref=lab_tech_rivera) → new_state="testing"; Audit Trail records transition_fired; transition_to_event updated. Returns "testing".
Tests complete; QA manager advances to QP review. fire_transition(actor_ref=qa_manager, instance_id, action="complete-tests", credential) → unguarded; fires; Audit Trail records. current_state = "qp-review".
QA manager opens the release gate. open_gate(actor_ref=qa_manager, instance_id, action="release", credential) → Permissions permitted (qa_manager holds workflows:open-gate); matched transition has guard "QP-sign-off"; not already open; ApprovalStep.submit(subject_ref="br-2026-0412:release", approver_ref="qp_director_santos", submitter_ref="qa_manager", scope="pharma:batch-release:qp-sign-off") → step_id="step-qp-0412-release"; Assignment.assign(task_ref=step_id, assignee_ref="qp_director_santos") → assignment_id="asgn-qp-0412"; maps written; Audit Trail records gate_opened. Returns {step_id, assignment_id}.
QP Director reviews and approves. decide_gate(actor_ref=qp_director_santos, instance_id, action="release", decision="approve", reason="Batch specification limits met; COA reviewed; QP sign-off granted under 21 CFR 211.68", credential=qp_credential) → no Permissions check (Approval Step Invariant 4 is the enforcement); gate_binding[(instance_id, "release")] → step_id; ApprovalStep.approve(step_id, decided_by="qp_director_santos", reason=...) → approved; Assignment.recall(asgn-qp-0412); Audit Trail records gate_decided. Returns approved.
QA manager fires the release transition. fire_transition(actor_ref=qa_manager, instance_id, action="release", credential) → Permissions permitted; matched transition is guarded; gate_binding[(instance_id, "release")] → step_id="step-qp-0412-release"; ApprovalStep.read({step_id}) → step state is Approved; composition asserts guard_satisfied = true; WorkflowStateMachine.fire(instance_id, "release", actor_ref="qa_manager", guard_satisfied=true) → new_state="released"; Audit Trail records transition_fired with guarded=true, step_id; transition_to_event updated. Check moot-gate cascade: current_state is now "released" (terminal); the "QP-rejection" gate was never opened, so no cascade is needed. Returns "released".
Attempt to fire after terminal state. fire_transition(actor_ref=qa_manager, instance_id, action="release", credential) → Permissions permitted; WorkflowStateMachine.current(instance_id) → "released" ∈ terminal_states; returns terminal.
Two years later — FDA Part 11 inspection. Inspector queries read_workflow({instance_id: "wf-batch-br-2026-0412"}). The composed view returns: workflow record; Workflow / State Machine history (5 entries: sampled → testing → qp-review → released, plus terminal); each transition’s Audit Trail event_id; the "QP-sign-off" gate’s Approval Step (Approved, decided_by=qp_director_santos, decided_at, decision_reason). The inspector calls AuditTrail.verify_record(event_id, payload) for the transition_fired event on the release transition and receives verified. The inspector confirms: (a) the batch moved only through declared states (Invariant 5); (b) the release transition fired with guard_satisfied=true and the bound step is in Approved state (Invariant 1); (c) the QP’s identity is attested under Part 11 §11.50 (Audit Trail Actor Identity). Control evidence is complete from the records alone.

Happy path — SOX §404 journal-entry posting workflow

A financial system governs posting of journal entries above the $5M materiality threshold. The declaration has states {draft, submitted, posted, rejected} with an unguarded submit transition (draft → submitted), a guarded post transition (submitted → posted, guard "controller-sign-off"), and an unguarded reject transition (submitted → rejected). The gate_spec binds "controller-sign-off" to {approver_ref: "controller_morgan", scope: "financial:journal-entry:post:materiality-tier-3"}.

JE-2026-0441: the preparer calls start_workflow; fires submit; calls open_gate(action="post"); the controller calls decide_gate(decision="approve"); the preparer calls fire_transition(action="post"). The composition verifies the controller’s Approval Step is in Approved, asserts guard_satisfied=true, and fires. Audit Trail records each action under sox_7_year retention. Seven years later, a SOX §404 audit queries the workflow and confirms Invariants 1, 2, and 6.

Rejection path — guarded transition attempted without open gate

The QA manager in the pharmaceutical scenario, after current_state = "qp-review", calls fire_transition(action="release") without having called open_gate first. At step 5a of fire_transition: gate_binding[(instance_id, "release")] does not exist; the composition returns gate-not-cleared. The Workflow / State Machine records no transition. No history entry is written. The QA manager must call open_gate first, then wait for the QP’s decision, then retry fire_transition.

Rejection path — guarded transition attempted with gate in Pending

The QA manager has opened the release gate (gate_binding set) but the QP has not yet decided. The QA manager calls fire_transition(action="release"). At fire_transition step 5b: ApprovalStep.read({step_id}) → state is Pending; the composition returns gate-not-cleared. No WorkflowStateMachine.fire call is made. The gate must reach Approved before the transition can fire.

Rejection path — unauthorized transition attempt

An actor lacking workflows:fire calls fire_transition. At step 1, Permissions.permitted(actor_ref, workflows:fire) → denied; returns permission-denied immediately. No Workflow / State Machine call is made. No Audit Trail entry is produced for the unauthorized attempt (see Edge cases — Audit Trail records of failed authorization attempts).

Moot-gate cascade — alternate transition leaves a gate unreachable

A purchase-order workflow has current_state = "awaiting-approval" with a guarded approve transition (guard "finance-sign-off") and an unguarded cancel transition, both departing from awaiting-approval. The finance director’s approval gate has been opened (gate_binding[(instance_id, "approve")] set, Approval Step in Pending). A process manager calls fire_transition(action="cancel"). The cancel transition is unguarded and fires successfully; new_state = "cancelled". The moot-gate cascade (step 7): the "approve" gate’s from_state = "awaiting-approval" ≠ "cancelled" = new_state; the gate is moot. The composition calls ApprovalStep.withdraw(step_id, withdrawn_by=initiator_ref, reason="Gate moot: ..."), Assignment.recall(assignment_id), and AuditTrail.record_action(action_ref=moot_gate_recalled, actor_ref=application_actor_ref, ...). The finance director’s in-tray no longer shows the approval task. The audit trail records the withdrawal and the reason.

Regulated adversarial scenarios

Three adversarial reads this composition must survive in regulated contexts:

Regulator audit — SOX §404 / FDA 21 CFR Part 11: prove declared-path and gate-cleared

An FDA inspector or SOX auditor demands evidence that process instance wf-batch-br-2026-0412 moved only through its declared states and that the qualified-person gate was genuinely cleared before the release transition fired. The auditor queries read_workflow({instance_id: "wf-batch-br-2026-0412"}) and receives the composed view. The auditor confirms: (a) every transition in the Workflow / State Machine history corresponds to a declared transition (read_declaration returns the immutable declaration; Invariant 5 — constituent Workflow / State Machine Invariant 3 — guarantees no undeclared transition could have produced a history entry); (b) the "release" history entry carries guard_satisfied: true and step_id pointing to the bound Approval Step; (c) ApprovalStep.read({step_id}) returns state: Approved, decided_by: "qp_director_santos", decided_at, and decision_reason; (d) Approval Step Invariant 4 guarantees decided_by matched approver_ref at the time of the approve call; (e) AuditTrail.verify_record(event_id, payload) for the transition_fired event returns verified. The auditor’s structural questions — did the batch move only through declared states? and was the release gate cleared by the named QP? — are answered from the records alone under Invariants 1, 5, and 6. No recourse to source code, runbooks, or developer narration is needed.

Disputed transition — party claims a guarded transition fired without its approval

An external party (an auditor, a counterparty, an investigator) claims that the "release" transition fired in instance wf-batch-br-2026-0412 without QP approval, or that an unauthorized actor advanced the process. The structural rebuttal:

For the “no approval” claim: the Workflow / State Machine history entry for the release transition carries guard_satisfied: true (Invariant 8 of the constituent — the atom records whether the caller asserted the guard). The composition’s gate_binding[(instance_id, "release")] maps to step_id="step-qp-0412-release". ApprovalStep.read({step_id}) returns state: Approved. Invariant 1 of this composition states that guard_satisfied = true was asserted by the composition only because the bound step was in Approved at the time of fire_transition step 5b. A forgery would require either (a) fabricating an Approved Approval Step record for a step whose approver_ref is qp_director_santos — foreclosed by Approval Step Invariant 4 (only the named approver may decide) and by the Audit Trail’s tamper-evident sealing — or (b) fabricating a Workflow / State Machine history entry with guard_satisfied: true — foreclosed by the Workflow / State Machine’s Invariant 5 (history append-only; storage-failure is the only non-success path for fire) and by Tamper Evidence sealing. Invariants 1, 3, and 5 together constitute the structural rebuttal.

For the “unauthorized actor advanced the process” claim: AuditTrail.verify_record for the transition_fired event returns the Actor Identity attestation, binding the actor reference to the action at the attested timestamp. Invariant 2 (Permission-gated process advancement) guarantees the firing actor held workflows:fire at the time of the Permissions check. An auditor confirms both.

Breach or incident investigation — reconstruct transitions and gate decisions during anomaly window

During a security incident (suspected credential compromise from 2026-05-01T00:00:00Z to 2026-05-03T23:59:59Z), the incident response team must determine which workflow transitions fired and which gates were cleared during the window. The team queries read_workflow({started_at: {after: "2026-04-25T00:00:00Z"}}) for all recently started workflows. For each instance, the team inspects the Workflow / State Machine history and — via transition_to_event — the corresponding Audit Trail event_ids. For each transition_fired event in the anomaly window, the team calls AuditTrail.verify_record(event_id, payload) to confirm integrity. Any failed-verification(tampered) response indicates a post-hoc modification — a forensic finding. For guarded transitions in the window, the team cross-references the bound Approval Step via gate_binding: ApprovalStep.read({step_id}) returns decided_by and decided_at, and the Audit Trail gate_decided event confirms the gate decision under the Actor Identity attestation. The team also queries the Permissions store for actors who held workflows:fire during the window; any transition fired by an actor whose grant was not active at the firing timestamp is a finding. Invariants 3 and 5 bound the forensic window precisely: the transition history is the complete ordered record of every step that advanced the process; the Audit Trail provides the integrity attestation for each.

Generation acceptance

A derived implementation of Stateful Workflow Execution is acceptable — in the regulator-acceptance sense — when an external auditor, given the composition’s emergent state plus the constituent stores, can do all of the following without recourse to source code, runbooks, or developer narration:

Audit-Trail-traversal-clearable checks

Verify the approval-gated-transition claim. For every Workflow / State Machine history entry whose matched declared transition carries a guard label (i.e., history entries with guard_satisfied: true): follow transition_to_event[transition_id] to the Audit Trail event_id and confirm it carries step_id in its data; follow gate_binding[(instance_id, action)] to find the bound step_id; confirm ApprovalStep.read({step_id}) returns state: Approved; confirm decided_by matches the gate_spec’s approver_ref for that guard label (Approval Step Invariant 4). A guarded history entry whose bound step is not in Approved, or whose decided_by does not match approver_ref, is a conformance failure under Invariant 1.
Verify only-declared-transitions and replay determinism. For every workflow instance: call WorkflowStateMachine.read_declaration(instance_id) and WorkflowStateMachine.history(instance_id). Confirm every {from_state, action, to_state} triple in the history corresponds to a declared transition. Replay the history in sequence_number order from initial_state and confirm it arrives at current_state. A history entry with a triple not in the declaration, or a replay that does not converge to current_state, is a conformance failure under Invariant 5 (constituent Workflow / State Machine Invariants 3 and 7). Confirm the declaration has not changed since start_workflow (Workflow / State Machine Invariant 1 — declaration immutability).
Verify audit completeness. For every workflow start, gate opening, gate decision, and transition firing recorded in the workflow store and Approval Step store: exactly one corresponding record_action event exists in the Audit Trail (action_ref ∈ {workflow_started, gate_opened, gate_decided, transition_fired, moot_gate_recalled}). The reverse direction also holds: every workflow-related Audit Trail entry corresponds to a record in the workflow store, gate_binding, or Approval Step store. No workflow action is invisible to the Audit Trail; no Audit Trail entry refers to an instance or gate that does not exist. Invariant 3 is the contract. Inherits Audit Trail’s atomicity surface (modulo the substrate’s Partial attestation on step failure edge case; the auditor alerts on orphan attestations referencing this composition’s action_ref values).
Verify gate assignment coverage. For every gate_binding entry whose bound Approval Step is in Pending state: confirm exactly one Active Assignment exists with task_ref = step_id and assignee_ref = approver_ref. For every gate_binding entry whose bound step is in a terminal state: confirm no Active Assignment exists for that step. Confirm moot gates (where the workflow’s current state is not the gate’s from_state) have been withdrawn and their Assignments recalled (or the gate was already decided before the workflow left the state). Invariant 4 is the contract.
Verify permission enforcement. For every workflow_started, gate_opened, fire_transition Audit Trail entry: confirm the actor_ref held the corresponding scope (workflows:start, workflows:open-gate, workflows:fire) in the Permissions instance at the time of the action, via the Audit Trail’s Actor Identity attestation and the Permissions store’s grant records. Invariant 2 is the contract.

Externally-clearable checks

Whether the gate_spec correctly maps to the regulatory requirements. The composition records the gate_spec declared at start_workflow and validates it structurally (every guarded transition named; every entry non-whitespace). It does not verify that the declared approver_ref for each guard label was the correct authority under the deployment’s regulatory policy. “Was qp_director_santos the required qualified person for batch BR-2026-0412 under 21 CFR Part 211?” is a calling-system policy question; the composition records the answer the calling system declared. Verification of the policy mapping (transition guard → required approver identity) requires the deployment’s role-authorization registry — typically a Permissions instance scoped to scope-approval grants, cross-referenced at the started_at timestamp. This parallels Multi-Party Approval’s Audit gaps for approver-set policy.
Whether the declared state machine itself matches the regulation’s required process. The composition records the declaration as supplied and enforces declared-transition discipline. It does not verify that the declared states and transitions are the correct process under the applicable regulation. “Does this declaration correctly represent the five-step batch-release process required by Part 211?” is a regulatory-process-design question answered by the deployment’s process documentation. Auditors verify this by reading the declaration alongside the relevant regulatory standard.
Whether the named approver was authorized to hold the approver role. The composition enforces that decided_by matched approver_ref (Approval Step Invariant 4) and that approver_ref was named in the gate_spec (checked at start_workflow). It does not verify that the named approver was the correct authority for the scope at the time of the gate decision. Cross-referencing approver_ref and scope against the deployment’s standing-authorization registry at started_at is an external audit check.

Edge cases and explicit non-goals

Multi-approver gates. A guarded transition requiring N approvers (all-of-N, M-of-N, one-of-N quorum) uses a Multi-Party Approval chain in place of a single Approval Step as the gate. The composition reads the chain’s terminal Approved state the same way it reads a single step’s Approved state — via the gate_binding pointing to the chain id rather than a step_id. The gate_spec entry for such a guard label names the chain’s chain_id (or a stable chain reference) rather than a single approver_ref; the open_gate action initiates a Multi-Party Approval chain rather than a single Approval Step. This multi-approver-gate variant is a composing enrichment of this composition, not part of the core single-approver-gate model. Deployments requiring multi-approver gates on any guarded transition should layer Multi-Party Approval for those gates.
Non-approval guard evaluation. This composition evaluates only approval-type guards — guards whose evaluation consists of checking whether a named actor has approved a specific subject under a specific scope. Guards whose evaluation requires a threshold check (an account balance exceeds a limit), a quorum count (N of M sensors reported above threshold), an external condition (an external service returned a green status), or a rules-engine decision are still the caller’s responsibility per Workflow / State Machine’s guard-evaluation edge case. The composition does not provide a generic guard-evaluation surface; it evaluates exactly one class: approval-step-based guards. A deployment that declares a guarded transition with a non-approval guard must supply guard_satisfied = true to WorkflowStateMachine.fire via a separate orchestration layer that is not this composition. Mixing approval and non-approval guards in the same declaration is a deployment-design choice; the composition owns only the approval-type ones.
Parallel / concurrent active states and fork-join. This composition has exactly one current state at all times, inherited from Workflow / State Machine’s Invariant 2 (exactly one current state). Parallel workflows — where an instance is in multiple active states simultaneously, with fork and join transitions — are out of scope. A Parallel Workflow fork-join composition (not yet in the library) handles that concept; this composition is the single-active-state declared-machine primitive.
Declaration versioning and sharing declarations across instances. The composition takes the declaration as a value at start_workflow and fixes it immutably per instance via Workflow / State Machine’s Invariant 1 (declaration immutability). Sharing one canonical declaration template across many instances — updating the template for new instances without re-supplying it at each instantiate — is handled by a Definition Registry (named in Workflow / State Machine’s edge cases). The calling system retrieves the current template from a registry and supplies it at start_workflow; this composition receives a value declaration.
Moot-gate cascade and return paths. The moot-gate cascade (step 7 of fire_transition) withdraws open gates for transitions whose from_state the workflow has left. If the declaration includes a return path to that from_state (e.g., a transition from released back to qp-review for a re-review), a gate that was moot when the workflow left may become relevant again. In this case, open_gate must be called again for the re-relevant transition; the prior gate has been withdrawn and cannot be re-used. This is consistent with Approval Step’s Invariant 3 (terminal absorption — a withdrawn step cannot be re-opened). The deployment must design its process declaration and gate-opening logic accordingly.
Cross-store consistency under partial failure. start_workflow writes to three stores in sequence (Workflow / State Machine constituent, workflow_store, Audit Trail). open_gate writes to three stores (Approval Step, Assignment, composition maps + Audit Trail). decide_gate writes to two (Approval Step, Audit Trail). fire_transition writes to two or three (Workflow / State Machine constituent, Audit Trail, optionally gate_binding cleanup on moot cascade). A failure mid-sequence leaves partial state. The recovery rules are stated per action under each action’s Partial-failure recovery note. The general principle: the load-bearing write (the constituent atom transition for fire_transition; the Approval Step submit for open_gate) is the write that determines whether the action semantically committed. Subsequent Audit Trail and map writes are recovery-amenable. An Audit Trail record_action failure after a load-bearing write surfaces as recording-failure to the caller and requires retry; the Audit Trail entry will be missing until retry succeeds, a gap in Invariant 3 the implementation must resolve.
fire_transition non-idempotency. WorkflowStateMachine.fire is not idempotent (two fire calls with the same (instance_id, action) both succeed if the transition is still available from the resulting state). Callers requiring at-most-once semantics under retry conditions must supply their own idempotency key at the orchestration layer; this composition does not provide one.
Audit Trail records of failed authorization attempts. A fire_transition, start_workflow, or open_gate call rejected at the Permissions check (permission-denied) leaves no Audit Trail entry by default. High-assurance deployments where failed authorization attempts are themselves auditable compose a Failed-Attempt Log pattern; the canonical composition’s audit surface is committed workflow actions, not attempted actions. This parallels Multi-Party Approval’s equivalent edge case.
Guard evaluation for non-approval guards is still the caller’s / Rules Engine’s obligation. Named explicitly in Non-approval guard evaluation above and in Workflow / State Machine’s edge cases. The composition evaluates only approval-type guards; all other guard evaluation paths remain the calling system’s or a composing Rules Engine’s responsibility.
Clock source for fired_at and decided_at. The composition sets timestamps at the receiving node’s wall clock when constituent atoms do not carry their own timestamp. Clock skew across distributed nodes can produce fired_at values that are not strictly monotonic across history entries; this is inherited from Workflow / State Machine’s clock-semantics edge case (sequence_number is the authoritative order source; fired_at is best-effort). For deployments requiring adversarially defensible timestamps on each transition, the Trusted Timestamping composing pattern is the resolution.
Concurrent fire_transition calls on the same instance. Two callers concurrently calling fire_transition on the same instance_id must be serialized; the implementation must hold a per-instance mutex at the composition layer as well as at the Workflow / State Machine constituent layer. A concurrent fire_transition and decide_gate on the same instance must also be serialized to prevent the composition from reading an Approval Step state that changes between the state read and the WorkflowStateMachine.fire call.
Non-repudiation, tamper-evidence, and retention. These properties are inherited via the Audit Trail substrate. Non-repudiable attribution is provided by Actor Identity; tamper-evidence of the event log is provided by Tamper Evidence; retention governance is provided by Retention Window. This composition does not re-derive any of these properties; it names them as substrate obligations and inherits the substrate’s composition-level invariants.
“Which approvals a transition should require” is the deployment’s business-rule layer. The gate_spec correctness — whether the declared approver for a guard label is the correct authority under the deployment’s regulatory policy — is not this composition’s contract to enforce. The composition enforces that gate_spec is structurally complete (every guarded transition named; every entry non-whitespace) and that the gate decision is made by the named approver (Approval Step Invariant 4). The policy question — whether the named approver was the right person — is an external audit check (Generation acceptance check 6).

Standards references

This composition is the structural form of what every multi-actor regulated workflow requires:

FDA 21 CFR Part 11 (Electronic Records; Electronic Signatures) — every transition in a Part 11 electronic records system is an electronic record; guarded transitions driven by approval gates constitute electronic signatures. Part 11 §11.50 requires signatures be attributable; §11.70 requires they be linked to records to prevent removal, substitution, or falsification. The composition’s Audit Trail substrate (Actor Identity providing cryptographic binding; Tamper Evidence providing the linking) satisfies both. The only-declared-transitions enforcement (Invariant 5) and the approval-gated-transition claim (Invariant 1) are the records-alone proof that §11.10 system access controls and §11.70 record integrity requirements were honored.
FDA 21 CFR Part 211 (Current Good Manufacturing Practice for Finished Pharmaceuticals) — batch release requires authorization by a Qualified Person or equivalent designated authority. A Workflow / State Machine-governed batch lifecycle with a QP approval gate on the release transition is the structural form of the Part 211 batch-release control. The guarded-transition record (history entry with guard_satisfied: true and bound Approved Approval Step) is the per-batch control evidence.
SOX (Sarbanes-Oxley Act) §404 (17 U.S.C. §7262) — Internal control over financial reporting. Process-control records for financial workflows (journal entry posting, purchase order approval, account reconciliation) must demonstrate that the required control steps occurred in the declared order and that each gate was cleared by an authorized actor. The composition’s records-alone process proof (Invariant 6) is the structural form of the SOX §404 control evidence requirement. Composes with Audit Trail’s SOX §802 retention obligation (7 years).
ISO 9001:2015 §8.5.1 (Control of production and service provision) — production and service provision activities must be controlled by documented procedures with controlled transition points. A Workflow / State Machine instance governing a production process is the documented procedure record §8.5.1 anticipates; the composition adds the human-gate enforcement and the regulated-audit substrate.
BPMN 2.0 (Business Process Model and Notation 2.0 — an international standard for modeling business processes, published by the Object Management Group) — this composition is the runtime form of a BPMN process diagram with human task gates. BPMN states map to declared Workflow / State Machine states; BPMN sequence flows map to declared transitions; BPMN human task gates map to the approval-step-gated transitions. The composition enforces the BPMN model’s declared process semantics at runtime.
ICH E6(R3) GCP (International Council for Harmonisation E6(R3) Good Clinical Practice — the global standard for clinical trial conduct) — clinical trial lifecycle events (protocol submission, IRB approval, deviation handling, trial closure) require documented approvals at defined points by named authorities. Stateful Workflow Execution is the structural form of the GCP-required documented approval trail.
ISO 13485:2016 §7.3 (Design and development) — medical device design changes require multi-disciplinary approval (design lead, quality, regulatory affairs, often clinical) at defined process gates. This composition’s guarded-transition model is the per-gate enforcement layer; Multi-Party Approval is the composing enrichment for gates requiring multiple approvers.

It inherits from:

The Audit Trail substrate — SOX §802, HIPAA (Health Insurance Portability and Accountability Act — US law governing protected health information) §164.530(j), PCI DSS (Payment Card Industry Data Security Standard) Requirement 10.5, ISO/IEC 27001:2022 §A.8.15 (logging) retention and integrity obligations, via the Audit Trail composition’s own standards inheritance.
Daniel Jackson, The Essence of Software — the composition discipline: Workflow / State Machine and Approval Step are freestanding atoms with orthogonal concepts; this composition is the wiring that makes them coherent in the regulated-workflow context.

Status

grounded on Final Critique 4 — 2026-06-04 (formal layer complete 2026-06-04 — TLA+ model stateful-workflow-execution.tla + buggy twin verified in tools/harness/; see Lineage §Formal model). Sonnet-drafted against an Opus plan, then Opus-gated through Pass 1 (GRID), Pass 2 (EOS — the substrate convention holds; the guard-evaluation re-convergence is tightly bounded to approval-type guards; no over-absorption), Pass 3 (Linus), and a Final Critique round: one foundational finding and one refining clarification, closed in-pattern (see Lineage notes). Regulated-pattern conventions (Regulated adversarial scenarios; Generation acceptance two-subsection split) baked in from the first draft. First composition to compose the Workflow / State Machine atom; the composition where guard evaluation re-converges. The formal-layer vote was YES; the derived TLA+ model — the approval-gated-transition claim (a guarded transition fires only when its bound Approval Step is Approved; the fire and audit-binding commit atomically), mirroring audit-trail.tla / chain-of-custody.tla — verifies green (25 states, all invariants hold) with two isolated buggy twins, each dedicated to one load-bearing invariant: stateful-workflow-execution-buggy.tla fires ungated (but audited) → breaks Invariant 1 (gate clearance) only, and stateful-workflow-execution-buggy-unaudited.tla fires gated (but unaudited) → breaks the audit-binding atomicity invariant only. (The twins were split 2026-06-04 after tools/harness/isolate.mjs flagged the original single combined twin — which fired both ungated and unaudited — as masking one invariant’s rejection behind the other’s shorter counterexample; gate clearance and audit atomicity are independent claims, so each earns a dedicated twin, the same discipline applied to Credential.) The English cleared the 92%-good threshold (foundational findings at zero) and the formal layer is discharged, so the composition is unqualified grounded.

Lineage notes

Regulated composition. Conventions — Regulated adversarial scenarios and Generation acceptance (with the two-subsection split: Audit-Trail-traversal-clearable and Externally-clearable) — inherited from the methodology directly (pressure-testing.md), baked in from the first draft. Multi-Party Approval is the primary structural twin: it composes Approval Step + Permissions + Assignment + Audit Trail (as substrate), the same constituent set as this composition minus the Workflow / State Machine spine. Its substrate convention, three-step chain-action shape, application-state and cross-atom map model, application_actor_ref/application_credential discipline, load-bearing-wiring-decision subsection style, cascade discipline, GA two-subsection split, and Lineage Structural-milestone paragraph are all mirrored here. Workflow / State Machine is the constituent whose guard-evaluation boundary this composition closes; its EOS Pass-2 boundary argument explicitly deferred guard evaluation to this composition as the designated re-convergence point.

Structural milestone. This composition (C10) retires the Stateful Workflow Execution *(forthcoming)* links in atoms/workflow-state-machine.md and atoms/approval-step.md. It is the first composition to compose the Workflow / State Machine atom, establishing the workflow category’s composition surface. It is also the composition where guard evaluation re-converges: Workflow / State Machine deliberately extracted guard evaluation as an EOS boundary (guards recur across many domains; each class has its own state machine); this composition closes the extraction for the approval-type guard class by binding each guarded transition to an Approval Step and asserting guard_satisfied = true only when the bound step is in Approved. The gate_binding map is the structural artifact that closes this gap — it is the application-layer state that the Workflow / State Machine atom correctly did not carry.

Formal-layer vote — initial author (Sonnet draft): YES. The load-bearing approval-gated-transition claim (Invariant 1: a guarded transition fires only when its bound Approval Step is Approved; the fire call and the Audit Trail event_id binding commit atomically) is an ordering and safety claim across two constituent stores (the Workflow / State Machine transition history and the Approval Step store) with an atomic audit-binding step. This is a TLA+ claim: the correct model is fire guarded transition ⟺ gate is in Approved state at the time of fire call, and the Audit Trail binding is written atomically with or immediately after the fire. The buggy twin is fire a guarded transition without reading the gate state (bare guard_satisfied = true from the caller), OR fire a guarded transition with the gate in Pending, OR fire the guarded transition but fail to write transition_to_event (non-atomic audit binding). Mirroring audit-trail.tla and chain-of-custody.tla. (Superseded 2026-06-04: the prose passes cleared and the TLA+ model landed and verifies — see the entry immediately below; this paragraph is preserved as the record of the vote as cast.)

Formal model — 2026-06-04: TLA+ authored and verified; pattern promoted to grounded. Derived model stateful-workflow-execution.tla + config stateful-workflow-execution.cfg, checked via tools/harness/check.mjs. What it checks: per guarded transition, gate (none/pending/approved/rejected — the bound Approval Step state), fired (the WorkflowStateMachine.fire happened), audited (the transition_to_event binding written). Two composition-level safety invariants under every interleaving: the load-bearing Invariant 1 (Inv1_GateClearance — fired ⇒ gate = approved: a guarded transition fires only when its bound gate is Approved; the composition evaluates the gate, never fires on a bare caller assertion) and Inv_BindingAtomic (fired ⇒ audited: no fired transition lacks its audit binding). The CORRECT model fires a guarded transition only on gate = approved and commits fired + audited in one atomic step; 25 reachable states, all invariants hold. Bounds/saturation: Gates = {g1, g2}; the property is per-gate local, insensitive to gate count. Buggy twin: stateful-workflow-execution-buggy.tla replaces the guarded fire with one guarded only on ~fired (ignores the gate — modelling a composition that trusts a bare caller-asserted guard_satisfied) and that sets fired without audited (non-atomic). From Init, FireGuardedBuggy(g) reaches fired ∧ gate = none ∧ ¬audited, violating both invariants; the checker rejects it at 3 states. This is the model’s load-bearing contribution: it shows mechanically that evaluating the gate (rather than trusting the caller) and committing the audit binding atomically are required, not decorative — a guarded transition firing without its gate cleared, or without its audit record, is reachably unsafe. Conflict-protocol outcome: none — the model corroborates the English; canonical English unchanged. Reproduce: cd tools/harness && node check.mjs ../../compositions/stateful-workflow-execution.tla (and … stateful-workflow-execution-buggy.tla --buggy).

Opus-led gating review — 2026-06-04 (Pass 1 GRID / Pass 2 EOS / Pass 3 Linus + Final Critique). Sonnet drafted against the Opus plan; Opus gated. One foundational finding and one refining clarification, closed in-pattern:

F1 — gate withdrawal authority contradicted Approval Step Invariant 5 — foundational (Pass 3). open_gate submitted each gate’s Approval Step with submitter_ref = the open_gate caller, but the moot-gate cascade (fire_transition step 7) and decide_gate(withdraw) both withdraw with withdrawn_by = initiator_ref — so whenever the gate-opener was not the workflow initiator, Approval Step Invariant 5 (only the submitter may withdraw) would reject the cascade unauthorized, leaving a moot gate un-withdrawable (an action wiring contradicting a constituent invariant). → The gate’s submitter_ref is now pinned to the workflow initiator_ref (the open_gate caller remains the audit actor on the gate_opened event); gate withdrawal — by the initiator via decide_gate(withdraw) or by the moot-gate cascade — is now authorized under Approval Step Invariant 5, matching Multi-Party Approval’s initiator-owns-withdrawal discipline.
F2 — workflows:open-gate scope — refining (Pass 3, design clarification). The draft introduced a dedicated workflows:open-gate Permissions scope rather than folding gate-opening into workflows:fire. Accepted as the right call and recorded as deliberate: gates open lazily throughout the workflow’s life (so binding to workflows:start would be wrong), and opening an approval gate is a distinct authority from advancing the process.

Pass 1 GRID clean (all composition sections present; reference graph intact — Workflow/State Machine, Approval Step, Permissions, Assignment, Audit Trail, Multi-Party Approval all exist). Pass 2 EOS clean: the substrate convention keeps Event Log / Actor Identity / Retention Window / Tamper Evidence transitive; non-approval guard evaluation stays the caller’s / a Rules Engine’s obligation (the composition evaluates only approval-type guards — the precise re-convergence of Workflow/State Machine’s deliberate extraction); multi-approver gates are a Multi-Party Approval composing variant, not re-derived quorum. The English clears the 92%-good threshold (foundational findings at zero); the TLA+ approval-gated-transition model is the remaining grounding prerequisite per the YES vote.