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

基于 TLA+ 形式化方法模型检验的治理状态机。十个状态、四位编码、零歧义。每一次转换都保证单比特变化。

治理状态机

Gray Code 有限状态机

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

每个智能体框架都有一个"安全"复选框，但没人能证明它有效。MAREF 的治理状态机用 TLA+ 规格对宪法红线做模型检验： 不变量在状态空间上验证、HALT 吸收、每次转换都单比特变化。

状态，永远明确。

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

HALT。无法撤销。

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

模型检验，就非承诺。

TLA+ 模型检验验证宪法红线不变量。收敛用 Lyapunov 式启发式跟踪。声明可复现，而非断言。

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

十个状态，每个状态使用 4 位 Gray Code 编码。相邻状态间仅变化一位，任何转换都不会落在歧义的中间地带。 TLA+ 模型检验对宪法红线不变量在这个状态空间上运行；HALT（状态 9）是吸收终止态。

三次。锁定。没有例外。

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

驱动状态机走向 HALT

from maref import GovernanceStateMachine, GovernanceState

sm = GovernanceStateMachine()
sm.transition(GovernanceState.OBSERVE, "start monitoring")

# HALT（状态 9）是吸收态——没有出边。
# 离开它需要明确、经认证的人工覆盖。

可以观察的收敛性。

Lyapunov 式收敛监控根据观测到的指标历史计算一个启发式稳定性指数，治理引擎跟踪错误指标是否随时间下行。这是你可以在公开基准测试套件里复现的运行时遥测——不是一个被断言的证明。

技术规格

状态机

10 个状态；HALT（状态 9）为吸收态

编码

4 位 Gray Code，汉明距离 = 1

形式化方法

TLA+ 对宪法红线不变量做模型检验

已验证性质

红线不可变、安全门完整性、审计完备、HALT 吸收

集成

GovernanceOverlay 类，pip install maref

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