# How to formally verify an agent governance framework with TLA+

> Source: <https://dev.to/maref/how-to-formally-verify-an-agent-governance-framework-with-tla-4ei0>
> Published: 2026-08-11 10:00:29+00:00

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

# 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](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."*