Model the agent as a transition system

A useful architecture begins with a formal object small enough to reason about. Let S be the set of runtime states, A the set of authorized actions, O the set of observations, and T a transition function. At step t, a policy proposes an action from the current state, an executor applies that action to the environment, an observation is normalized, and the reducer computes the next state. In compact form: proposal a_t = π(s_t), observation o_t = E(a_t), and state s_{t+1} = T(s_t, a_t, o_t). The model usually implements part of π. Trusted application code implements validation, E, and T.

This resembles a partially observable decision process because the runtime never sees the full environment. A database query may be stale, a web page incomplete, a test nondeterministic, or a user request ambiguous. Do not respond to partial observability by pretending the state is complete. Record provenance, freshness, confidence, and unresolved uncertainty. The policy can then choose an information-gathering action, while the runtime can require escalation when uncertainty crosses a risk threshold.

The formal model pays for itself through invariants. A safety invariant states something that must never become false: total spend does not exceed the run budget; a write cannot occur without the required approval; a tool result cannot alter the instruction hierarchy; the sandbox cannot access production credentials; a refund count cannot exceed one. A liveness property states that something desirable eventually happens under stated assumptions: every admitted run eventually reaches a terminal state; an approved action is eventually attempted or explicitly canceled; a waiting run eventually expires. Safety is not the same as success, and liveness is not “keep trying forever.” A system that never acts may preserve safety while failing its purpose. A system that retries forever violates bounded liveness.

State should be normalized rather than represented only as a conversation transcript. A transcript is chronological text optimized for the model, not an authoritative data model. It mixes user claims, tool results, instructions, intermediate hypotheses, and summaries. Normalized state separates immutable run metadata, goal specification, current facts, action history, budget counters, approvals, artifacts, and terminal status. The model may receive a projection of that state, but the projection can be rebuilt and tested.

Actions form an algebra. Read actions gather evidence and should have no intended external side effects. Propose actions create candidate plans or artifacts inside a workspace. Write actions change durable external state. Approval actions request or consume human authorization. Terminal actions claim success, failure, cancellation, or escalation. Classifying actions by effect makes policies comprehensible. For example, the runtime can allow ten reads, three sandbox writes, one approval request, and zero production writes for a low-trust run.

Observations also need a closed schema. A tool call should return status, typed data, bounded diagnostic text, provenance, latency, and retry guidance. Raw HTML, shell output, or exception text is untrusted input, not a new instruction. The normalizer truncates or stores large artifacts by reference, removes secrets, classifies errors, and preserves a digest of the full result. This prevents the context window from becoming the database and gives the reducer stable inputs.

The transition function is where policy becomes product behavior. It increments counters, checks invariants, records events, updates derived facts, and selects a terminal reason when a guard fires. It must reject impossible transitions such as moving from succeeded back to running, spending a consumed approval twice, or changing the goal after a write has begun. A compare-and-set version or transactional update prevents two workers from concurrently applying different next states.

Plans deserve a limited role. A plan is a hypothesis about future actions, not a command queue that bypasses later checks. Every action is revalidated against current state immediately before execution. This matters because tools can change the environment, users can revoke authorization, budgets can be consumed, and earlier assumptions can fail. Long plans are useful for communication and dependency analysis, but the controller commits one bounded step at a time.

Hierarchical state machines help organize complex runs. A top-level run may be queued, running, waiting, succeeded, failed, canceled, or escalated. The running state may contain substates such as gathering evidence, proposing, executing, and verifying. Orthogonal regions can track authorization and budget independently. Harel's statecharts introduced hierarchy, concurrency, and broadcast concepts to tame reactive-system state explosion. The implementation need not draw a statechart at runtime, but it should preserve the same explicit structure.

Formal methods are most valuable around costly ambiguity. Model a small abstraction of approvals, retries, cancellation, and duplicate delivery in TLA+ or another state-machine tool before production. Check invariants across interleavings rather than testing one happy path. The goal is not to prove the language model correct. It is to prove that, regardless of proposals, the controller cannot cross specified authority and budget boundaries.

An architectural review should therefore ask: What is authoritative state? Which transitions are deterministic? Which components are nondeterministic? What invariants are checked before and after an effect? Can a stale worker commit? Can every waiting state expire? Are terminal reasons mutually exclusive? Can the same event be replayed without calling the model or tool again? If these questions have precise answers, the agent is becoming an engineered system rather than a prompt with privileges.