注：某些较旧的链接可能仍指向之前的项目名称。
这是什么
一个可执行、由攻击者驱动的安全回归测试套件：- 每一条声明都带有一个可在有限状态空间上运行的模型检查。
- 许多声明都配有一个成对的负向模型，它会为现实中的某类漏洞生成反例轨迹。
模型存放位置
模型保存在一个单独的仓库中：vignesh07/openclaw-formal-models。
该仓库目前无法访问（截至撰写本文时，GitHub 返回“Repository not found”）。如果对你来说它仍然有问题，请先在 OpenClaw 维护者频道中询问当前的位置，再假定这些模型已经被移除。
注意事项
- 这些是模型，不是完整的 TypeScript 实现——模型与代码之间可能存在偏差。
- 结果受 TLC 探索的状态空间限制。绿色并不意味着在所建模的假设和边界之外也具备安全性。
- 某些声明依赖于明确的环境假设（例如，正确的部署和正确的配置输入）。
复现结果
在先前记录的模型仓库无法公开访问时，复现说明不可用。在尝试下面的目标之前，请在 OpenClaw 维护者频道中询问经过验证的当前位置。 目前这个仓库还没有集成 CI；未来的迭代可以添加在 CI 中运行的模型，并提供公开产物（反例轨迹、运行日志），或者为小规模有界检查提供一个托管的“运行此模型”工作流。主张与目标
网关暴露与开放网关配置错误
主张： 在没有认证的情况下，绑定到回环地址之外可能导致远程被攻陷，并增加暴露面；根据模型假设，令牌/密码可以阻止未认证攻击者。
另见模型仓库中的
docs/gateway-exposure-matrix.md。
节点 exec 管道（最高风险能力）
主张：exec host=node 需要：(a) 节点命令白名单以及已声明的命令，且 (b) 在配置了审批时需要实时审批；在模型中，审批使用令牌化以防止重放。
配对存储（DM 门控）
声明： 配对请求会遵守 TTL 和待处理请求上限。入口门控（提及与控制命令绕过）
主张： 在需要提及的群组上下文中，未经授权的控制命令不能绕过提及门控。路由与会话密钥隔离
主张： 来自不同对端的私信不会合并到同一会话中，除非显式关联或进行了配置。v1++ 模型：并发、重试、追踪正确性
围绕真实世界故障模式进一步收紧保真度的后续模型：非原子更新、重试，以及消息扇出。配对存储并发与幂等性
声明： 配对存储即使在交错执行下也能强制执行MaxPending 和幂等性——检查再写入必须是原子/加锁的，刷新也不能创建重复项。具体来说：并发请求对某个通道的数量不能超过 MaxPending，并且对同一 (channel, sender) 的重复请求/刷新不会创建重复的存活待处理行。
入口追踪关联与幂等性
声明： 当一个外部事件变成多个内部消息时，摄取过程会在扇出过程中保持追踪关联，并且在提供方重试下保持幂等性。每个部分都保持相同的追踪/事件标识；重试不会重复处理；如果缺少提供方事件 ID，则去重会回退到一个安全键（例如 trace ID），以避免丢弃不同事件。路由 dmScope 优先级与 identityLinks
声明：dmScope 优先级和 identityLinks 的行为是确定性的：默认的 main 作用域会让单个拥有者的多个 DM 共享一个滚动会话（个人代理默认行为），而任何配置为隔离的作用域（per-peer、per-channel-peer、per-account-channel-peer）都会严格分离 DM 会话。特定频道的 dmScope 覆盖优先于全局默认值；identityLinks 只会在显式关联的分组内合并会话，不会跨无关的对端合并。多用户收件箱应当选择隔离作用域（运行时安全审计在检测到多用户 DM 流量时会建议这样做）。