DEV Community

Open Human
Open Human

Posted on

How to formally verify an agent governance framework with TLA+

#tlaplus #agents #governance #python

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) → ...
Enter fullscreen mode Exit fullscreen mode

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/):

  1. State reachability — every governance state is reachable from the initial state (BFS witness, validator.py).
  2. Transition determinism — no two transitions fire from the same state on the same input.
  3. Halt absorption — once the machine enters HALT, it can never leave (HaltGovAbsorbing PROPERTY in MarefJoint34MC.cfg).
  4. Safety gate integrity — unsafe transitions are blocked at the gate (SafetyGateIntegrity, INV-002 in MAREF_ConstitutionalRedLines.tla).
  5. 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
Enter fullscreen mode Exit fullscreen mode

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)