Block 开源 buzz：多 Agent 通信平台的两处形式化验证
本文基于 buzz 仓库 commit 8342dfc（2026-08-04）梳理，该项目仍在高频迭代，具体行为以仓库 https://github.com/block/buzz 最新代码与文档为准。
这两份规格里最值得抄走的不是 TLA+ 语法，而是一条纪律：每加一条不变量，先想办法让它红一次。 buzz 的 docs/spec/MultiTenantRelay.tla 把十三个故意写坏的实现变体（M1 到 M13）写进了文件头注释，其中七条还标了 Confirmed red 与实测反例轨迹的长度；docs/spec/MultiTenantAuth.spthy 把四条会让定理失败的变异规则以注释形式原样保留在正文里，其中三条明确写着 DO NOT ENABLE。一条断言如果从没有见过失败，它证明的可能只是它自己。
一、先认人：这是 Block 开源的 buzz，不是别的什么
buzz 是 Block 开源的一个多 Agent 通信平台，许可证 Apache-2.0（Copyright 2026 Block, Inc.）。它建在 Nostr 之上——Nostr 是一套去中心化消息协议，一条消息就是一个事件：JSON 结构，带作者公钥、kind 数字、内容、标签和一段签名；中继（relay）是负责存储与转发事件的服务器；用户身份不是账号密码，而是一对密钥，客户端拿私钥自己签名，中继只验签。仓库 README 这样定位自己：人和 Agent 在同一个工作区里协作，中继归你自己所有；一个 community 就是用户按 URL 访问到的那个工作区。
对 AI 工程读者来说，这个组合的含义是：Agent 和人在同一张消息网络里，用同一套事件格式和同一种签名身份说话，Agent 的权限边界就是它那把私钥被授予的范围。
形式化验证的意思很朴素：把系统写成一个数学模型，让工具去穷举模型能到达的所有状态（或攻击者能构造的所有消息序列），检查某条性质是不是恒成立。这篇和站内已有几篇的分工是这样的——对手验证 谈的是让另一个 Agent 来挑你的毛病，完成前验证 谈的是交付前那道自查关口，回归测试 谈的是用例集怎么防止改坏，而本篇是它们的上游：在写实现之前，先把”什么叫做对”用机器可判定的方式写死。
| 组成部分 | 它负责什么 | 仓库位置 | 你什么时候会碰到它 |
|---|---|---|---|
| 多租户中继 TLA+ 模型 | 把 N 个无状态中继进程共享一个 Postgres 的隔离性写成状态机不变量 | docs/spec/MultiTenantRelay.tla | 想看隔离到底被定义成了什么 |
| TLC 跑模型的配置 | 固定有限规模的常量与对称性约束 | docs/spec/MultiTenantRelay.cfg | 自己复现模型检查时 |
| 鉴权协议 Tamarin 模型 | 令牌铸造、主机绑定、社区签名密钥、审计链在攻击者面前的性质 | docs/spec/MultiTenantAuth.spthy | 关心令牌泄漏与密钥被攻破的后果 |
| 散文版规格 | 系统模型、公理、定理、先前工作、实现对应关系 | docs/multi-tenant-relay.md | 读模型之前的必要背景 |
| 一致性清单 | 逐个界面列出今天的行为、租户来源、需要的索引与迁移门禁 | docs/multi-tenant-conformance.md | 判断这套设计要动多少代码 |
| 推送网关的有界可执行模型 | 用 Python 穷举授权/配额/重放的有限状态 | docs/formal/STATEFUL_GATEWAY.md 与 docs/formal/nip-pl/ | 看轻量级形式化怎么落到已上线功能上 |
| 配对协议模型 | 设备配对的符号化安全模型 | crates/buzz-core/src/pairing/NIP-AB.spthy | 想找同一套写法的第二个样例 |
二、TLA+ 那半：隔离被定义成标签不能外流
多租户这件事的常见写法是：给每张表加一列 community_id，查询都带上 WHERE community_id = $1，再补一层 Postgres 行级安全（RLS，数据库按策略自动过滤行）。MultiTenantRelay.tla 的文件头明说，这里的证明义务不止是”不会返回带错 community_id 的行”，而是非干扰性：每个状态元素和每个观测都带上影响过它的社区标签，任何带着连接所属社区之外标签的值都不许流进这个连接看得到的界面。核心不变量 Inv_NonInterference 就一行：任意观测的 labels 必须是它自身 community 的子集。
关键在于”观测”被定义得比返回行宽得多。模型里的 ObsKinds 有五类：查询结果行、写入结果、经过消毒的错误、审计链头、鉴权判定。这五类都要背标签义务。于是几件平时不当成安全面的事都被抓进来了：
写冲突是观测。WriteDuplicate 分支返回 Duplicate 这个结果本身就泄露”这个事件 id 在本社区已存在”。模型要求冲突检查按 (community, id) 而不是全局 id 做——文件里专门留了一个 GlobalConflictRows(id) 算子并注释为”故意写坏的版本”，用于变异 M3，注释记录的结果是 Safety 在深度 3 被违反，反例是一个 B 社区作用域的写入结果观测却带着 A 社区的标签。换句话说，唯一索引少带一列租户键，功能测试一条都不会红，泄的却是存在性预言机。
错误消息是观测。.cfg 把客户端可见的错误固定成九个字符串的字母表（auth-required、restricted、invalid、duplicate、pow、rate-limited、blocked、error、frame-too-large），并要求这类观测的标签集为空——错误文本必须与租户无关。变异 M6 就是让错误带上原始标签。
投影重建是内部工作。重建可以扫全库所有社区，但不许发出任何观测；租户读到的要么是自己那部分投影行，要么是它的子集，要么什么都没有（重建中途）。
再往上一层是租户到底由谁决定。模型给出的答案是 ResolveTenant(host, ch)：带频道的操作从服务端持有的频道到社区映射解析，不带频道的操作（资料、私信、长文、列表这类没有 h 标签的事件）从连接的主机名解析。客户端声称的社区是对抗性输入，一律忽略。三个建模常量把这件事钉死：HostA、HostB，以及映射到 NoCommunity 哨兵的 HostBad——未映射的主机不落到默认租户，而是直接失败。更狠的是，带频道的操作要求主机映射与频道映射一致，A 主机上递交 B 频道的事件属于混淆代理，写入、鉴权、重复探测三条路径全部 fail-closed，只回一个消毒错误并记一次查询故障。
Safety 这个总不变量是十三个合取：一个 TypeOK 加十二条 Inv_ 开头的不变量；Next 里列了二十三个动作。.cfg 的规模很小：两个社区、五个频道、三个主机、一个 actor、一个 worker、一个消息 id、两个审计值，观测集上限 2，外加对称性约减。散文规格 docs/multi-tenant-relay.md 记录的运行结果是穷举完成、16,226,016 个不同状态、深度 13，并直说这个配置”是刻意设计的快速非空泛测试台，不是部署规模”。
三、Tamarin 那半：先把最坏情况写进模型
MultiTenantAuth.spthy 换了一个世界。Tamarin 是符号化协议验证器，默认对手是 Dolev-Yao 攻击者：网络完全由攻击者控制，所有消息都能被读取、篡改、重放、拼接，唯一做不到的是破解密码学原语本身。用 grep 数一下这个文件：22 条规则、32 条 lemma，其中 14 条是 exists-trace（存在性引理，用来证明某条正常流程真的跑得通，防止安全引理因为前提永不成立而空过）。
这份模型最值得看的是它主动把灾难写成规则。Compromise_Client_Key 直接把客户端私钥输出给攻击者，Compromise_Community_Signing_Key 把社区签名密钥输出给攻击者，Leak_Token 把铸造出来的承载令牌输出给攻击者。定理不是”这些不会发生”，而是”这些发生之后，损失被关在哪里”。leaked_token_blast_radius_contained 断言令牌即便泄漏，被授权的社区仍等于铸造时盖章的社区；other_community_key_compromise_does_not_admit 断言 B 社区签名密钥被攻破，也不足以把某个公钥塞进 A 社区的成员名单——因为成员列表事件的签名原像里绑定了社区 id，接受时是按解析出来的社区去查签名密钥，而不是按事件里声称的那个。
主机绑定在这里有一个漂亮的建模技巧。Use_Token_ChannelLess 在授权那一刻发出一条 ChannelLessResolved(tok, comm, host, comm) 动作事实，把”实际使用的社区”和”主机绑定的社区”塞进同一条事实里；对应的 lemma 只读这一条事实并断言两者相等。好处写在注释里：断言只依赖单条事实，反例就是一次规则实例，而不是跨多条事实的联结推理或攻击者状态重构，于是变异一旦引入，falsify 很快。带频道的那条路径用 ChannelBearingResolved 复制了同样的手法。
文件里那四条注释掉的 MUTATION_ 规则是同一套纪律的另一半：把令牌用途改成读客户端声称的社区、把主机绑定忽略掉、把频道无关路径改成信令牌盖章、把成员准入重绑到另一个社区。每条都注明了期望哪条 lemma 变红；其中两条还记下了实测结果——忽略主机绑定那条被一条 14 步反例证伪，改信客户端声称社区那条被一条 15 步反例证伪，注释里写明跑的是 Tamarin 1.12.0 与 Maude 3.5.1。另外两条只写了预期变红的 lemma 和推理，没有留步数，这本身也说明这份纪律是人工维护的，不是自动跑出来的。
同样值得记的是它的坦白。审计链那一节的注释直接写着：这是目标形态，不是今天的实现，当前 buzz-audit 是一条全局链，多租户安全需要 N 条按社区标记的独立链。
四、边界与代价：这套东西明确不管什么
规格自己列了一份不证清单，比证了什么更值得读。
它不证活性与性能。查询能不能满足延迟预算、热分区会不会拖慢，是压测的事，不是定理的事。
它不证 Postgres 的正确性。行级安全的执行、MVCC 快照隔离、ON CONFLICT DO NOTHING 的语义都是公理，证的是在这些之上的组合。密码学也一样：BIP-340 的 Schnorr 签名不可伪造性、NIP-98 请求绑定、事件 id 哈希的抗二次原像，是 Tamarin 模型的等式理论，不重新证明。
它不证物理资源隔离。缓冲池、autovacuum、查询计划统计、热分区尾部、连接池延迟这些带宽受限的时序信道，被明确列为 C1 类豁免，写在文件头上而不是藏起来。
它不证接口之上的客户端泄漏。如果一个用户同时在两个社区，客户端界面、分享链接或日志把 A 社区的事件 id 带了出来，这个人就能拿着 id 去 B 社区探测。规格说复合索引这条封堵让探测问不出东西，但同时点名：换成更弱的索引形状，这个面就是客户端的义务，不是中继的。
还有两件事必须说清楚。第一，这是先证后写。docs/multi-tenant-relay.md 顶上标着 draft，.tla 第一行写的是 proposed，文件头的”今天的 buzz”一节列出了现状：crates/buzz-db/src/event.rs 的查询结构里没有 community_id，crates/buzz-db/src/channel.rs 的 get_accessible_channel_ids 会把库里所有开放频道并起来，crates/buzz-relay/src/state.rs 今天是进程全局状态。这些不是被证明为安全，恰恰相反，它们被点名当成变异靶子。今天的边界仍然是”一个中继进程一条 DATABASE_URL”。
第二，这套验证没有进 CI 门禁。仓库 .github/workflows/ 下有 16 个工作流文件，grep 一遍 tamarin、tla2tools、spthy、.tla，一个引用都没有；docs/formal/nip-pl/ 下那六个 Python 模型也没有被任何工作流调用。规格与代码的同步，目前靠人。
散文规格里还有一处少见的自曝：NIP-98 的重放检查用的是进程内 seen-set，容量 10000、TTL 120 秒，按每副本各存一份。文档直说，仓库里 deploy/ 目录中 replicaCount: 3 的高可用示例按原样部署是不满足这条防重放前提的，除非运营方改成共享 seen-set 或按签名头做粘性路由，并且明确推荐前者、指出后者依赖请求头字节完全一致因而脆弱。
五、上手清单：容易踩的六处
把规格读成实现说明。 会踩是因为文件躺在 docs/spec/ 下、语气是定理式的，读起来像在描述现有行为。避的方法是先读 docs/multi-tenant-relay.md 的 Scope and Non-Goals 与 Implementation Correspondence 两节，那里逐条对照”模型要求什么、今天是什么样”。
照抄 .cfg 跑一遍绿了就下结论。 会踩是因为那个配置只有一个 actor、一个 worker、一个消息 id，观测集上限 2，还开了对称性约减；跑绿只说明这个有界窗口里没找到反例。避的方法是把它当非空泛测试台用：改完模型先按 M1 到 M13 的说明把变异一条条替换进去，确认每条都能红，再去看绿的那次。
误调用文件里的坏算子。 UnscopedAccessible、GlobalConflictRows、GloballyAdmitted、UnscopedDirectIdRows、DefaultOpenAuthCommunity 这些定义和真算子并排放在同一个文件里，注释都点明是故意写坏的版本、只在复现某条变异时替换进去，UnscopedAccessible 那条写得最直白：正确规格不调用它。会踩是因为名字看着挺正常。避的方法是改模型前先搜一遍谁引用了它们。
把唯一索引当成性能问题。 会踩是因为把 UNIQUE 建在事件 id 上而不是 (community_id, …, id) 上，所有功能用例都通过，泄漏发生在写冲突的分支上。避的方法是把租户列当成键的一部分强制进流程：唯一约束、外键、缓存 key、搜索索引、pub/sub 频道名，一致性清单的迁移门禁第 1 条和第 3 条就是干这个的。
只在读路径加过滤。 会踩是因为直觉上隔离等于 SELECT 带条件，而模型把错误字母表、审计链头、鉴权判定、重复写结果一并算成观测。避的方法是先把”客户端能观察到的所有取值域”列成一张表，再逐个问：这个取值受谁影响。
低估密钥自持的产品代价。 会踩是因为演示环境里密钥是自动生成的，感觉不到成本。实际情况是身份即密钥对，模型里客户端私钥被攻破是一条正常规则；私钥丢失等于身份丢失，没有找回按钮，社区签名密钥被攻破则该社区的成员名单可被伪造，定理只保证不外溢到别的社区。避的方法是把密钥托管、轮换、撤销当作第一天的需求。Agent 这一侧同理，它拿的是同一套签名身份，权限设计要当成硬约束——可参考最小权限设计与状态机与自由发挥的取舍。
收束：三个问题和一个阅读顺序
拿这三个问题去问自己手上的系统：客户端能观察到的取值域有哪些，是否每一个都被问过”它受谁影响”；每条断言有没有见过至少一次失败，失败长什么样，记在哪；哪些性质你其实没有证、只是相信，这份清单写在别人看得到的地方了吗。
接着读代码的顺序建议是：先 docs/multi-tenant-relay.md 建立词汇表，再 docs/spec/MultiTenantRelay.tla 的文件头注释（M1 到 M13 那段就是整套设计的失败模式索引），然后 docs/spec/MultiTenantAuth.spthy 的规则区，最后 docs/multi-tenant-conformance.md 那张大表——它是这四份文件里最像工程任务清单的一份。
本篇属于一个把开源多 Agent 通信平台 buzz逐层拆开讲的系列，整体地图见 buzz 是什么：Block 开源的多 Agent 通信平台全景图；沿着这条线往下，还可以看 Block 开源 buzz 多 Agent 平台的设备配对：一份 NIP 规范加一份形式化模型 和 Block 开源多 Agent 平台 buzz：一致性检查器怎么对齐实现。