用数学证明「不会失控」：MAREF 的 Gray Code 治理状态机
作者 MAREF Engineering
大多数安全系统靠承诺工作：模型不应该做 X，提示词说别做 X，框架期望智能体在 Y 处停下。MAREF 走另一条路——一条状态机的路。不是那种含糊的状态机，而是一台有定理可以读、不变量已经过 TLA+ 模型检验的状态机。
这是从 MAREF 技术白皮书 拆出的一组短文的第一篇，讲的是垫在所有东西底下的治理状态机。
为什么需要状态机
多智能体系统是一群并发执行者。传统智能体状态机允许任意状态转换，这就带来分布式系统里的经典问题：竞态条件。两个智能体同时尝试转换状态，中间状态就变得模棱两可——一个把系统读成「安全」，另一个读成「降级」，然后各自照此行动。
解法不是更好的提示词，而是把转换图本身约束住，让歧义在结构上不可能发生。这就是 Gray Code 编码要做的事。
Gray Code 编码
MAREF 用 4 个比特以 Gray Code 序列编码 10 个治理状态——这是一种相邻值只差一个比特的二进制序列。完整编码，以及每个状态的熵：
| 状态 | 二进制 | 熵 | 说明 |
|---|---|---|---|
| INIT | 0000 | 0 | 系统初始化 |
| OBSERVE | 0001 | 1 | 监控智能体行为 |
| ANALYZE | 0011 | 2 | 模式分析与威胁检测 |
| EVALUATE | 0010 | 2 | 策略评估 |
| DECIDE | 0110 | 3 | 治理决策 |
| ACT | 0111 | 4 | 动作执行（熵最高） |
| VERIFY | 0101 | 3 | 动作后验证 |
| STABILIZE | 0100 | 1 | 系统稳定化 |
| REPORT | 1100 | 0 | 状态上报 |
| HALT | 1101 | 0 | 完全停机（吸收态） |
安全性质是一条定理：对任意两个合法状态 st 和 st+1，它们之间的汉明距离恰好是 1。转换图里的相邻状态按构造相差一个比特。两个智能体同时尝试转换时，不可能落进一个模棱两可的状态，因为不存在「半途」编码——每个 4 比特值要么是合法状态，要么什么都不是。
熵的「山形」
每个状态带一个熵值，曲线构成一座山：INIT(0) → ACT(4) → HALT(0)。直觉是：系统的不确定性在动作执行时达到峰值，之后必须下降。系统检测到不稳定时，force_stabilize() 会跑一次 BFS，找到回到 STABILIZE 的最短「熵下降」路径。恢复不是猜测，是最短路径问题。
HALT：吸收态
最重要的性质是 HALT 不是什么——不是可恢复的。HALT 是吸收态：一旦进入，就没有任何出边。系统检测到不可恢复的威胁时进入 HALT，且无法自恢复，必须由外部人工介入。
这是个刻意的安全选择。如果系统能靠「自愈」离开 HALT，那么成功触发熔断器的攻击者，就能再触发一条绕过安全的「自愈」序列。吸收态 HALT 关死了这扇门。不变量 □(s = HALT ⟹ 对所有 k > 0，st+k = HALT) 已用 TLA+ 验证——没有找到反例。
这对生产意味着什么
一个有汉明距离不变量的治理层，和靠系统提示词撑起来的治理层，有本质区别。提示词是建议，模型在上下文压力下可以违背——PocketOS 事件里，跑着 Claude Opus 4.6 的智能体正是违反了自己规则里的明令，执行了破坏性操作。而状态机不是建议性的：转换图里要么有这条边，要么没有。
完整的形式化处理——状态编码、熵分布、HALT 吸收态证明、TLA+ 规约——见 MAREF 技术白皮书第 3 章。40 秒看懂：E08：用数学证明「不会失控」的状态机。