StateM distinguishes transition checks across four distinct tiers of evidentiary strength to prevent structured declarations from being mistaken for verified proof:

1. **Command and Predicate Checks**: Evaluated directly by the host runtime, providing independently reproducible evidence (subject to the correctness of the command or predicate).
2. **Manual Checks**: Require an explicit operational decision or approval from a user or human operator.
3. **Checklist and Message Checks**: Require the agent to acknowledge specified obligations; these serve as structured self-attestations rather than independent verification.
4. **LLM Review Checks**: Provide a separate qualitative semantic judgment without deterministic verification guarantees.

This evidentiary hierarchy ensures that self-attestations remain auditable and visible while reserving objective verification for deterministic or host-evaluated gates.

Taxonomy of State Transition Checks by Evidentiary Strength

In StateM, all phase changes use the core operation `goto TARGET`, which executes an ordered, six-step transition protocol:

1. **Edge Verification**: Verify that the requested transition edge from the current state to `TARGET` exists.
2. **Exit Check Evaluation**: Evaluate the current state's `before_transfer` exit checks.
3. **Persistence and Out-Hook**: Run the current state's configured persistence or `out_hook` operations.
4. **Edge Condition Evaluation**: Evaluate edge guards and edge-specific transfer hooks.
5. **State Commit & Logging**: Commit the target state and append the transition event to execution history only if all required pre-commit steps succeed.
6. **Target Setup & In-Hook**: Create the target-state entry and execute its `in_hook`.

If any required pre-commit check or hook fails, execution remains in the source state and records the failure, permitting the agent to inspect the unmet condition and retry.

StateM Ordered Transition Protocol

StateM implements a state transition model characterized as checked, logged, and recoverable rather than fully transactional. When advancing state via `goto TARGET`, the runtime delays committing the target state until all pre-commit checks and hooks succeed. If a failure occurs, execution remains halted in the source state and writes a failure record, allowing the agent to inspect and repair the deficiency.

However, because hook execution interacts with external tools and host processes, StateM cannot perform an automated ACID rollback of arbitrary external side effects. Instead, recovery relies on restoring durable StateM execution logs and executing configured, idempotent repair routines.

Checked and Recoverable Transition Semantics

In stateful agent harnesses, a state functions as a contract boundary governing phase completion, verification, and transition gating. While the state prompt defines the expected internal work of the phase, the runtime enforces explicit exit conditions before permitting a transition. An exit hook (`out_hook`) persists progress, updates receipts, or prepares artifacts for the subsequent phase, while a pre-transfer block (`before_transfer`) evaluates configured exit conditions. If a check fails, the run remains in the source state to enable inspection and repair rather than silently propagating unverified work or incomplete handoffs into later phases.

State as a Contract Boundary

University of Michigan - Ann Arbor

Ch.1 Operational Reliability and Verification - Engineering Deterministic Runtimes and Verification for Autonomous Agents @ University of Michigan - Ann Arbor

Operational Failure Modes: Control-Signal Dilution and Mutable-State Ambiguity - Engineering Deterministic Runtimes and Verification for Autonomous Agents @ University of Michigan - Ann Arbor

Verification Typologies and Transition Protocols - Engineering Deterministic Runtimes and Verification for Autonomous Agents @ University of Michigan - Ann Arbor

Learn Before

Related

Learn After