简要总结
Formal Verification (Security Models)
这页说明书像一张“安全保证书”，它告诉我们OpenClaw这个系统有多安全。它用一种特别的“模型检查”方法，像玩一个“找错误”的游戏，来检查系统在遇到坏人时会不会出错。这页适合你想知道OpenClaw是怎么保护自己，或者想自己动手运行这些检查游戏的时候看。
五岁小孩版解释
这页讲的是OpenClaw的“形式化验证”，你可以把它想成是给系统做一次非常非常严格的“安全体检”。它不是检查真正的软件代码，而是用一个叫“模型”的简化版本来模拟系统，看看在各种情况下，坏人能不能钻到空子。这个体检报告会告诉我们系统在哪些方面是安全的，但也要记住，它检查的不是全部。
重要的事情要先知道：
- 这些“模型”是玩具版的系统，不是真的软件，所以玩具和真玩具之间可能会有点不一样。
- 这个检查游戏只在一定的“游戏地图”范围内玩，检查通过了（显示“绿色”），不代表在所有地方都安全。
- 有些检查结果，是假设我们正确地搭建了系统、正确地设置了规则才成立的。
如果你想自己玩这个“检查游戏”： 你需要先准备好游戏盘（模型），然后运行检查命令。就像这样：
- 准备游戏盘：打开电脑上的“终端”或“命令窗口”，输入
git clone https://github.com/vignesh07/openclaw-formal-models来下载游戏。 - 进入游戏盘：输入
cd openclaw-formal-models走进去。 - 运行游戏：输入
make <target>来开始检查。这里的<target>就是下面要说的各种检查游戏的名字。运行前，你的电脑需要安装好 Java 11 或更新的版本。
现在，我们来玩几个具体的“检查游戏”：
这些游戏的名字都叫 make 后面加一个单词。有些游戏我们期待它通过（显示绿色），有些我们故意让它失败（显示红色），来证明我们的检查是有效的。
网关暴露检查：检查系统的大门（网关）是不是关好了，没有让坏人从外面直接进来。
- 绿色游戏（应该通过）：
make gateway-exposure-v2和make gateway-exposure-v2-protected - 红色游戏（应该失败）：
make gateway-exposure-v2-negative
- 绿色游戏（应该通过）：
节点运行管道检查：检查一个叫
nodes.run的很厉害的功能，是不是被安全地锁起来了，需要得到允许才能用。- 绿色游戏：
make nodes-pipeline和make approvals-token - 红色游戏：
make nodes-pipeline-negative和make approvals-token-negative
- 绿色游戏：
配对存储检查：检查“配对”请求会不会太多，或者存得太久。
- 绿色游戏：
make pairing和make pairing-cap - 红色游戏：
make pairing-negative和make pairing-cap-negative
- 绿色游戏：
入口门控检查：检查在群里，是不是必须@某人才能发特殊命令，坏人不能偷偷绕过。
- 绿色游戏：
make ingress-gating - 红色游戏：
make ingress-gating-negative
- 绿色游戏：
路由/会话隔离检查：检查你和不同朋友的私聊，是不是分开的，不会混到一起。
- 绿色游戏：
make routing-isolation - 红色游戏：
make routing-isolation-negative
- 绿色游戏：
还有更高级的检查游戏（v1++）： 这些游戏检查更复杂的情况，比如很多人同时操作、网络消息重发等。
配对存储并发检查：检查很多人同时申请“配对”时，系统会不会数错人数，或者给同一个人创建了多个申请。
- 绿色游戏：
make pairing-race,make pairing-idempotency,make pairing-refresh,make pairing-refresh-race - 红色游戏：
make pairing-race-negative,make pairing-idempotency-negative,make pairing-refresh-negative,make pairing-refresh-race-negative
- 绿色游戏：
入口追踪检查：检查一个从外面来的消息，在系统里变成很多个小任务时，它们是不是还属于同一个“家庭”（有相同的追踪ID），并且不会因为网络重发而被处理两次。
- 绿色游戏：
make ingress-trace,make ingress-trace2,make ingress-idempotency,make ingress-dedupe-fallback - 红色游戏：
make ingress-trace-negative,make ingress-trace2-negative,make ingress-idempotency-negative,make ingress-dedupe-fallback-negative
- 绿色游戏：
路由优先级检查：检查私聊的规则，是不是先听每个聊天室自己的特殊规定，再听通用规定。只有明确设置了“身份链接”的朋友，私聊才会合并到一起。
- 绿色游戏：
make routing-precedence和make routing-identitylinks - 红色游戏：
make routing-precedence-negative和make routing-identitylinks-negative
- 绿色游戏：