Security 导读
形式化验证：OpenClaw 安全策略的机器可检查证明
这页不是文档，而是一套可运行的 TLA+ 模型，用于验证授权、会话隔离、工具门控和配置安全等安全属性。先跑 `make gateway-exposure-v2` 等目标，看绿色通过和红色反例；注意模型与 TypeScript 实现可能存在偏差，通过不代表实际系统绝对安全。
先讲这一页到底在解决什么
形式化验证：OpenClaw 安全策略的机器可检查证明
这页不是文档，而是一套可运行的 TLA+ 模型，用于验证授权、会话隔离、工具门控和配置安全等安全属性。先跑 `make gateway-exposure-v2` 等目标，看绿色通过和红色反例；注意模型与 TypeScript 实现可能存在偏差，通过不代表实际系统绝对安全。
第一站
🧪 先把它当成“带攻击者视角的安全回归测试”
这页写得很诚实：它是模型检查，不是终局证明。
TLA+/TLC
像把规则写成可跑的棋盘，看看会不会走出坏局面。
negative model
像故意搭一条坏路，看机器能不能抓到反例。
绿色不等于绝对安全
因为模型是有限棋盘，不是整个宇宙。
第二站
📦 结果怎么跑出来
官方建议你去单独的模型仓库里 clone，再用 TLC 和 make 复现。
git clone https://github.com/vignesh07/openclaw-formal-models像把模型沙盘搬回自己桌上。
make <target>像把某个安全场景单独拉出来跑一遍。
Java 11+
像告诉你沙盘需要什么底座才能转起来。
第三站
🔐 这页最值钱的是它挑的几个重点风险
Gateway 暴露、nodes.run、错误配置，这些都是“模型里最容易翻车的门”。
Gateway exposure
像大门没锁好，远程风险直接变高。
nodes.run
像最高风险的能力按钮，必须双重确认。
一句话
这页的价值，是提前抓出“什么配置一错，安全边界就歪了”。