Safety you can verify.
Not just promise.
A governance state machine verified with TLA+ formal methods. Ten states, six bits, zero ambiguity. Every transition single-bit by construction.
Gray Code State Machine
Hamming distance = 1 on every transition. Mathematically verifiable governance.
Every agent framework has a "safety" checkbox. None of them can prove it works. MAREF's governance state machine verifies its constitutional red-line invariants with TLA+ model checking: invariants checked across the state space, HALT absorbing, every transition single-bit by construction.
Unambiguous state. Always.
Six-bit Gray code encoding guarantees Hamming distance = 1 between adjacent states. No transition is ever ambiguous.
HALT. And nothing can undo it.
Three consecutive failures trigger an absorbing halt state. No agent, process, or race condition can override it.
Checked, not claimed.
TLA+ model checking verifies constitutional red-line invariants. Convergence is tracked with a Lyapunov-style heuristic. The claims are reproducible, not asserted.
A state machine a mathematician would trust.
Ten states, each with a 6-bit Gray code encoding. Because adjacent states differ by exactly one bit, no transition can land in an ambiguous middle ground. TLA+ model checking verified this across every possible path. The state space is finite, complete, and fully explored.
Formal verification: 5 theorems, 10 states, 0 unreachable states
Three strikes. Locked. Period.
The CircuitBreaker watches every safety decision. Three failures in any time window trigger HALT. This is not a soft warning. HALT is an absorbing state — once entered, it requires an explicit, authenticated human override to leave. No agent, no pipeline, no race condition can escape it.
from maref import CircuitBreaker, HALT
breaker = CircuitBreaker(
threshold=3,
window_seconds=300,
on_halt=HALT # absorbing, no auto-recovery
)
# After 3 failures: state → HALT
# Requires human override to leaveConvergence that comes with a receipt.
Lyapunov-style convergence monitoring computes a heuristic stability exponent from observed metric history,
and the governance engine tracks whether error metrics trend downward over time.
It is reproducible runtime telemetry from the public benchmark suite — not an asserted mathematical proof.
What is formally verified: the constitutional red-line invariants, checked with TLA+ model checking.
Convergence tracking: Lyapunov-style stability exponent from metric history, monotonic downward trend