How to formally verify an agent governance framework with TLA+

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 inMarefJoint34MC.cfg ). - Safety gate integrity - unsafe transitions are blocked at the gate ( SafetyGateIntegrity , INV-002 inMAREF_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." Top comments (0)