Formally, a StateM runbook is defined as a tuple:

mathcal{B} = (mathcal{S}, s_0, mathcal{S}_T, mathcal{E}, Phi)

where:

• $\mathcal{S}$ denotes the finite set of phase-level states,
• $s_0 \in \mathcal{S}$ is the initial state,
• mathcal{S}_T subseteq mathcal{S} is the set of terminal states denoting completed execution,
• $\mathcal{E} \subseteq \mathcal{S} \times \mathcal{S}$ is the set of directed, permitted transitions between states, and
• $\Phi(s)$ is the state specification mapping each state $s \in \mathcal{S}$ to its phase-local prompt, entry and exit hooks (in_hook, out_hook), transfer checks (before_transfer), and references to state-local artifacts.