Safety you can prove.
Not just promise.
A governance state machine verified with TLA+ formal methods. Ten states, six bits, zero ambiguity. Every transition mathematically provable.
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 is the first with a TLA+ mathematical proof: five theorems verified, zero unreachable states, every transition deterministic 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.
Proven, not promised.
Five TLA+ theorems verified. Lyapunov convergence. Sperner completeness. Every claim has a mathematical proof.
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 stability analysis proves the governance engine converges toward a safer state over time. Not "probably." Not "empirically." Mathematically. The Lyapunov function V(x) = xᵀPx guarantees the error rate decreases monotonically toward a provable minimum. The proof is public. Anyone can verify it.
Lyapunov function: V(x) = xᵀPx, V̇(x) ≤ -α‖x‖²