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?
