From Math to Machine: MAREF's Gray Code Governance State Machine

Most safety systems work on promises: the model shouldn't do X, the prompt says don't do X, the framework expects the agent to stop at Y. MAREF takes a different route — the route of a state machine. Not a hand-wavy one. A state machine with a theorem you can read, and an invariant that TLA+ model-checking has verified.

This is the first post in a short series drawn from the MAREF technical whitepaper. It covers the governance state machine that sits underneath everything else.

---

Why a State Machine at All

A multi-agent system is a collection of concurrent actors. Traditional agent state machines allow arbitrary state transitions, which creates a classic distributed-systems problem: race conditions. Two agents try to transition the system at the same time, and the intermediate state is ambiguous — one reads the system as "safe," the other as "degraded," and both proceed accordingly.

The fix isn't better prompts. It's constraining the transition graph itself so that ambiguity is structurally impossible. That's the job of the Gray Code encoding.

The Gray Code Encoding

MAREF encodes its 10 governance states in 4 bits using a Gray Code sequence — a binary sequence where consecutive values differ by exactly one bit. The full encoding, with the entropy of each state:

The safety property is a theorem: for any two valid states s_t and s_t+1, the Hamming distance between them is exactly 1. Adjacent states in the transition graph differ by one bit, by construction. Two agents attempting simultaneous transitions can't land in an ambiguous state, because there is no "half-way" encoding — every 4-bit value is either a valid state or nothing.

The Entropy Mountain

Each state carries an entropy value, and the curve forms a mountain: INIT(0) → ACT(4) → HALT(0). The intuition is that system uncertainty peaks during action execution and must decrease afterward. When the system detects instability, force_stabilize() runs a BFS to find the shortest entropy-decreasing path back to STABILIZE. Recovery isn't a guess — it's a shortest-path problem.

HALT: The Absorbing State

The most important property is what HALT is not — recoverable. HALT is an absorbing state: once entered, no outgoing transitions exist. If the system detects an unrecoverable threat, it enters HALT and cannot self-recover. It requires external human intervention.

This is a deliberate security choice. If the system could "heal" itself out of HALT, an attacker who managed to trip the circuit breaker could then trigger a healing sequence that bypasses security. Absorbing HALT closes that door. The invariant □(s = HALT ⟹ s_t+k = HALT for all k > 0) was verified with TLA+ — no counterexamples found.

What This Means in Practice

A governance layer backed by a Hamming-distance invariant is qualitatively different from one backed by a system prompt. A prompt is a suggestion a model can override under context pressure — exactly what happened in the PocketOS incident, where an agent on Claude Opus 4.6 executed a destructive action against its own stated rules. A state machine is not advisory: the transition graph either has an edge or it doesn't.

The full formal treatment — state encoding, entropy profile, HALT absorbing-state proof, and the TLA+ specifications — is in Section 3 of the MAREF technical whitepaper. Watch it in 40 seconds in E08: Mathematically Proven State Machine.