安全，可以证明。
不只是承诺。

基于 TLA+ 形式化方法验证的治理状态机。十个状态、六位编码、零歧义。每一次状态转换都可以数学证明。

治理状态机

Gray Code 有限状态机

每步跳转汉明距离 = 1，数学可验证的治理状态转换

每个智能体框架都有一个"安全"复选框，但没人能证明它有效。MAREF 的治理状态机是第一个通过 TLA+ 数学证明的： 五大定理已验证、零不可达状态、每次转换都是确定性的。

状态，永远明确。

六位 Gray Code 编码保证相邻状态间汉明距离恒为 1。任何转换都不会落入模糊地带。

HALT。无法撤销。

连续三次失败触发吸收态 HALT。任何智能体、进程或竞态条件都无法覆盖它。

有证明，就非承诺。

五大 TLA+ 定理已验证。Lyapunov 收敛、Sperner 完备性。每个声明都有数学证明。

数学家也会信任的状态机。

十个状态，每个状态使用 6 位 Gray Code 编码。相邻状态间仅变化一位，任何转换都不会落在歧义的中间地带。 TLA+ 模型检查在所有可能路径上验证了这一点。状态空间有限、完备、全探索。

三次。锁定。没有例外。

断路器监控每次安全决策。任意时间窗口内三次失败触发 HALT。这不是一个软警告。 HALT 是吸收态——一旦进入，需要明确的、经过验证的人工覆盖才能退出。

CircuitBreaker 转入 HALT

from maref import CircuitBreaker, HALT

breaker = CircuitBreaker(
    threshold=3,
    window_seconds=300,
    on_halt=HALT  # 吸收态，无自动恢复
)

# 3 次失败后: state → HALT
# 需要人工覆盖才能退出

带着收据的收敛性。

Lyapunov 稳定性分析证明治理引擎随时间向更安全的状态收敛。不是"也许"，不是"经验上"， 数学上。Lyapunov 函数 V(x) = xᵀPx 保证错误率单调递减至可证明的最小值。证明是公开的，任何人都可以验证。

技术规格

状态机

10 个工作状态 + HALT 吸收态

编码

6 位 Gray Code，汉明距离 = 1

形式化方法

TLA+ 模型检查

定理

5 — Lyapunov 收敛、Sperner 完备性、状态可达性、转换确定性、暂停吸收

集成

GovernanceOverlay 类，pip install maref

安全，可以证明。 不只是承诺。