Why verify agent governance at all? Multi-agent systems are hard to reason about. A circuit breaker that "should" kick in, a state machine that "should" never skip a state — these are the kind of things you can prove, not just hope. Over the past year we've built multi-agent systems on CrewAI, AutoGen, and LangGraph. Getting agents to do things was never the hard part. The hard part was the question nobody had a good answer for: when an agent acts on its own, what stops it from crossing a line? This post walks through how we formalized our agent governance state machine with TLA+ and model-checked its safety invariants. The full specs live in the MAREF repo (Apache-2.0, pip install maref ). Why a Gray Code state machine? A naive governance state machine can skip states or jump unpredictably. We wanted a state space where every transition is a provably single-bit step — no skipped states, no hidden jumps. That's what a Gray Code gives you: consecutive values differ by exactly one bit (Hamming distance = 1). For a 4-bit FSM: 0 (0000) → 1 (0001) → 3 (0011) → 2 (0010) → 6 (0110) → ... If a transition ever jumps two bits, it's a bug by construction — the model checker catches it. The 5 model-checked invariants The README claims 5 invariants; here's what they actually are in the spec (files in src/formal/ and gray-code-fsm/ ): State reachability — every governance state is reachable from the initial state (BFS witness, validator.py ). Transition determinism — no two transitions fire from the same state on the same input. Halt absorption — once the machine enters HALT , it can never leave ( HaltGovAbsorbing PROPERTY in MarefJoint34MC.cfg ). Safety gate integrity — unsafe transitions are blocked at the gate ( SafetyGateIntegrity , INV-002 in MAREF_ConstitutionalRedLines.tla ). Red line immutability — constitutional red lines cannot be changed at runtime ( RedLineImmutability , INV-001). What the CI actually runs The formal-verify.yml workflow runs the real TLC model checker on every push to the formal specs. It verifies four specs, not just one: Spec File What it checks Gray Code FSM MarefLiteModel.tla TypeOK + HaltGovAbsorbing + TerminalsAbsorbAgent Consensus MAREF_Consensus.tla Byzantine bounds, quorum integrity, trust-weight correlation Constitutional Red Lines MAREF_ConstitutionalRedLines.tla RL-001..005 (red-line immutability, safety gate, audit completeness) Test Integration MAREF_TestIntegration.tla Cross-border consistency, prompt-rot detection All types are kept finite (bounded integer/string domains) so TLC can fully enumerate the state space instead of timing out. One subtlety worth sharing: TLA+ liveness ( <>P ) is universal over behaviors, so "state reachability" can't be a TLC PROPERTY for a non-deterministic model. We use a BFS validator.py for reachability witnesses and reserve TLC for the universal invariants. This distinction is easy to get wrong the first time. Try it yourself pip install maref # The specs are in the repo: # gray-code-fsm/MarefJoint34.tla — joint governance FSM # src/formal/MAREF_ConstitutionalRedLines.tla — constitutional invariants # gray-code-fsm/MarefJoint34MC.cfg — TLC model checker config Full spec: https://github.com/maref-org/maref/tree/main/gray-code-fsm When NOT to use TLA+ Formal verification is not free. We use it only for the governance core — the few hundred lines that enforce safety boundaries. The orchestration layer (10k+ lines) uses unit tests and integration tests instead. Model checking state spaces explodes fast; keep the verified core small and finite. Notes All types are kept finite (bounded integer/string domains) so TLC can fully enumerate the state space. Liveness properties like "reachability" use a BFS validator instead of TLC <>P (which is universal over behaviors and can't witness existence). Apache-2.0, no commercial restrictions. This is the first in a series on building governance for autonomous agents. Follow for the next one: "Why your multi-agent system needs a circuit breaker."