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
).
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 README claims 5 invariants; here's what they actually are in the spec (files in src/formal/
and gray-code-fsm/
):
validator.py
).HALT
, it can never leave (HaltGovAbsorbing
PROPERTY in MarefJoint34MC.cfg
).SafetyGateIntegrity
, INV-002 in MAREF_ConstitutionalRedLines.tla
).RedLineImmutability
, INV-001).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.
pip install maref
Full spec: https://github.com/maref-org/maref/tree/main/gray-code-fsm
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.
<>P
(which is universal over behaviors and can't witness existence).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."