Block 开源多 Agent 平台 buzz：一致性检查器怎么对齐实现

2026-08-05

本文基于 buzz 仓库 commit 8342dfc（2026-08-04）梳理，该项目仍在高频迭代，具体行为以仓库 https://github.com/block/buzz 最新代码与文档为准。

模型跑绿只证明模型自己自洽，它对你的 Rust 代码一个字都没说。 buzz 这个由 Block 开源、建在 Nostr 协议之上的多 Agent 通信平台（仓库地址 https://github.com/block/buzz，Apache-2.0，Copyright 2026 Block, Inc.），在 docs/spec/ 下放了 TLA+ 规范和配置，也在 crates/buzz-conformance 下另做了一层运行时一致性检查：让线上代码在关键关口吐出一串结构化的 trace，再用一个刻意不认识生产代码的检查器去判这串 trace 模型收不收。这篇讲的就是这条缝怎么缝。

先把几个协议底座的名词说清楚，后面不再解释。Nostr 是一套消息协议：每条消息是一个由发送方私钥签名的事件（event），服务端叫中继（relay），职责是收下事件、验签、存储、按订阅条件分发。身份就是那对密钥，没有账号系统，私钥丢了等于身份丢了，谁也补不回来。buzz 仓库 README 这样定位自己：人和 Agent 共享同一批房间的自托管工作区，无论作者是人还是进程，消息、反应、工作流步骤、评审批准、git 事件都是同一条日志里的签名事件。在 buzz 的模型里，一个社区（community）就是用户按 URL 到达的那个工作区，docs/multi-tenant-conformance.md 把这条规则写死为「URL 主机名是权威的社区选择器」。形式化验证在这里指的是：把系统状态和状态转移写成数学模型，再用工具穷举状态空间检查不变量是否恒真。

一、模型证完了，缝还在哪

docs/spec/ 目录下有五个文件：MultiTenantRelay.tla 和它的 MultiTenantRelay.cfg、GitOnObjectStore.tla 和 GitOnObjectStore.cfg、还有一份 MultiTenantAuth.spthy。前者的模块头把证明义务写得很清楚：主证明义务不是「不返回带错 community_id 的行」，而是把非干扰性编码成标签/污点不变量——每个状态元素和每次观测都带上影响它的社区标签，任何标签在连接已解析社区之外的值都不得流入这条连接的观测接口。文件里列了 Inv_NonInterference、Inv_ReadConfinement、Inv_HostBindingFence、Inv_AdmissionFence、Inv_SanitizedErrors 等一串不变量，还专门列了一张变异测试清单（M1 到 M13），用来防止模型变成空转：比如 M2 是「WriteInsert/AuthCheck 用客户端声称的社区而不是 ChannelCommunity(channel)」，M8 是「丢掉主机与频道的一致性围栏」。

问题在于，TLC 把这些不变量全跑绿了，证明的只是那份 .tla 文本自洽。真正要跑在服务器上的是 crates/buzz-relay 里几千行 Rust。规范里写「解析出的社区来自主机绑定」，实现里那个变量到底是从 TenantContext 拿的还是从事件的 h 标签拿的，模型不知道。这就是那条缝：规范和实现共用一个名字，但不共用一行代码。

crates/buzz-conformance/src/lib.rs 的文件头注释直接把这个立场写成了北极星：不要问模型过没过，要问运行中的代码吐出的 trace 模型收不收。同一份注释也马上把话说死——这个 crate 不是证明，trace 一致性只检查你真的跑过的那些执行。

二、一条 trace 从关口流到检查器

整条链路只有四步，每一步都能在仓库里点开看。

第一步，关口投影。crates/buzz-relay/src/handlers/ingest.rs 的 ingest_event 在进入真正的入库逻辑前，先用 state_for_request(tenant, auth.pubkey()) 构造一份抽象状态。这个 AbstractState 只有三个字段：resolved_community（服务端解析出的社区，来源写死为 TenantContext::community()）、bound_host（绑定该解析的主机标签）、actor（认证公钥的前 16 位十六进制）。payload、事件 id 全文、签名、公钥全量、墙钟时间，一律不进 trace。TRACE_SCHEMA.md 给出的理由是：actor 前缀对客户端而言本来就是哈希（Schnorr X-only 公钥），前缀不会多暴露任何东西，同时省掉一个哈希依赖。

第二步，动作记录。每个决策点吐一个 TraceStep，结构是 { schema_version, action, state_after }。TraceAction 是个九元枚举：WriteInsert、WriteInsertGlobal、WriteDuplicate、SanitizedError、AuthCheck、ReadMessageRows、ReadByIdRows、ReadHostFeedRows，加上一个不属于规范的 ImplBug。前八个在 lib.rs 的文档注释里逐一标注了它对应 MultiTenantRelay.tla 的哪个动作。

第三步，回放判决。crates/buzz-conformance/src/checker.rs 的 check_trace 拿到一串步骤：先看空不空（空的直接判覆盖率违约），再校验 schema_version 与 crate 里的 SCHEMA_VERSION 相等，然后用第一步的 state_after 引导出 ModelState，逐步跑 check_step，最后做覆盖检查。判据本身在 transitions.rs，模块头注释写得很硬：它只读 crate 内的 trace 模式和规范文本，不 import buzz-relay、buzz-db、buzz-auth 或任何可能与发射端共享同一个归一化 bug 的生产 crate。

组成部分	它负责什么	对应仓库位置	你什么时候会碰到它
trace 模式 + `Tracer` trait	定义步骤/动作/抽象状态的形状，是发射端与检查端唯一的契约	`crates/buzz-conformance/src/lib.rs`	新增一类决策点、要加字段时
规范转移关系重写	把 `Next` 的每条动作义务翻成 Rust 判据	`crates/buzz-conformance/src/transitions.rs`	规范改了、要同步判据时
回放引擎	引导模型、逐步判决、做覆盖检查	`crates/buzz-conformance/src/checker.rs`	排查一条 trace 为什么红
关口投影与 `EmitGuard`	把 relay 的真实决策翻成步骤，并守住「不发射也算错」	`crates/buzz-relay/src/conformance/mod.rs`	接一个新的对外处理器时
两种 tracer	生产用 `NoopTracer`，测试与 CI 用 `JsonlTracer`	`crates/buzz-relay/src/conformance/tracers.rs`	想在某次跑动里真的留下 trace 时
固定 trace	四份入库的 JSONL，正例一份、反例三份	`crates/buzz-conformance/tests/fixtures/`	改模式后要同步刷新时
能力边界说明	明说这层不管什么	`crates/buzz-conformance/LIMITS.md`	有人拿绿灯当安全承诺时
模型本体	不变量与变异清单	`docs/spec/MultiTenantRelay.tla`	要判断某个判据到底源自哪条不变量

仓库里 crates/ 下一共 28 个 crate，buzz-conformance 是其中体量最小的之一：src/ 只有三个文件，加两份说明文档（TRACE_SCHEMA.md 和 LIMITS.md）和一个 tests/ 目录。这个体量本身是设计的一部分——判据小到能被人整个读完，才谈得上「独立」。

三、四种红灯，和为什么覆盖率违约最要紧

transitions.rs 定义的 TransitionError 有四个变体，对应四类完全不同的病。

StateMismatch：state_after 与引导出的模型不符。check_step 开头三个判断分别比对 resolved_community、bound_host、actor，任何一个在一次请求中途变了都红。它抓的是「请求处理到一半租户上下文被重新赋值」，或者某个步骤压根不是从 TenantContext 里发出来的。

IllegalTransition：动作在当前模型状态下不被允许。目前咬得最狠的一条是 AuthCheck：当判决是 Allow 而客户端声称的社区不等于已解析社区时，直接红，注释里点名这就是 M2 和 M8 的落点。反过来，Deny 配任何声称值都放行——规范把 Deny 建模成「主机不同意」或「不可达」的兜底，检查器刻意不在这里加戏。

NonInterference：三个读动作共用的行标签围栏。判据只有一句话：row_communities 里任何一个标签不等于已解析社区就红。check_row_labels 的注释解释了为什么参数是 Vec 而不是 Set——如果 relay 把同一条外来行返回两次，检查器照咬；如果发射端把外来标签去重成一条，检查器还是照咬。外来标签出现几次不重要，出现过就是全部的判据。

CoverageBreach：这条是命门。checker.rs 的文件头把它叫做检查器的另一半工作：场景要提前声明它必须走到哪些关键动作，走不到就红。没有这一层，一个悄悄删掉某个发射点的回归会照样过关——trace 只是变短了而已。Scenario 结构体因此有两个字段，一个是 trace，一个是 required_critical_actions。另外两种触发方式是：trace 为空，以及 trace 里出现了 ImplBug。

ImplBug 从哪来？crates/buzz-relay/src/conformance/mod.rs 里的 EmitGuard。它在关口入口处 arm 一次，返回一个守卫和一个 CountingTracer 包装器；请求路径照常调 record，包装器顺手把计数加一。守卫析构时如果计数还是零，就往底层 tracer 上写一条 ImplBug 步骤。ingest_event 里那次 arm 传的名字是 ingest_event_exited_without_trace，任何没发射就返回的分支都会被这条 Drop 逮住。

有个细节很值得抄：Tracer trait 上的 enabled() 默认返回 true，但 CountingTracer 强制委派给内层。mod.rs 里为此专门写了一个测试 counting_tracer_delegates_enabled_to_inner，注释把两个方向的后果都列了——包在丢弃型 tracer 外面却答 true，热路径上那次只为 trace 服务的 channels 查询就白跑；包在真 tracer 外面却答 false，被门控的发射点会被跳过，于是 EmitGuard 会对本来正确的关口报违约，甚至用一个预期内的违约盖住一个真的。两种错都是静默的。

四、两条不许走的近路

这层检查值不值钱，全押在两条纪律上。

近路一：复用生产类型。 CommunityLabel 是 conformance crate 自己的 newtype，明确不复用 buzz_core::CommunityId。lib.rs 给了两条理由：其一，CommunityId 故意没有 From<Uuid>、没有 Serialize、没有 Deserialize，就是为了让它无法从客户端输入里凭空造出来，为了检查器方便而给它加上 Serde 等于在生产围栏上开洞；其二，模式与生产类型零机械耦合，一个有 bug 的生产类型才没法把 bug 洗进检查器。转换只发生在关口那一行：CommunityLabel::from_uuid(*tenant.community().as_uuid())。

近路二：在发射时就把违规归一化掉。 TRACE_SCHEMA.md 列了三条投影铁律。一是客户端声称的社区必须和已解析社区分开记录，规范说「解析的赢」，但 trace 必须两个都留着，否则 M2 咬不动；claimed_community_from_event 就是专门去事件 h 标签里取那个声称值的。二是行标签是不去重、不按已解析社区过滤的 Vec。三是错误理由是三元闭字母表（Restricted / Invalid / ServerError），sanitized_reason_for 把 relay 的 IngestError 一一映射过去，多出第四个变体会让这个 match 不再穷尽，编译期就红。

读侧的行标签怎么来，是这两条纪律最容易翻车的地方，仓库的处理是 project_row_community：

match row_channel_id {
    None => Some(*resolved),
    Some(ch) => channel_communities
        .get(&ch)
        .map(|cid| CommunityLabel::from_uuid(*cid.as_uuid())),
}

关键在于 row_channel_id 取自行自己的 channel_id，不是查询的过滤条件，所以一条带频道的行没法伪装成无频道行来躲开这次查表。查不到怎么办？返回 RowCommunityProjection::MissingLookup，调用方 record_read_message_rows 把它落成一条 ImplBug，也就是覆盖率违约——而不是悄悄替换成已解析社区。注释把这个判断说得很直白：如果缺表时静默替换，这道关口就是空转的。

反例固定件长这样，是仓库里 bad_foreign_row_leak.jsonl 的原文一行（这里为便于阅读做了换行，内容未改）：

{"schema_version":1,
 "action":{"type":"read_message_rows",
           "channel":"cafe0000-0000-0000-0000-000000000010",
           "row_communities":["bbbb0000-0000-0000-0000-000000000002"]},
 "state_after":{"resolved_community":"aaaa0000-0000-0000-0000-000000000001",
                "bound_host":"a.example.test",
                "actor":"0123456789abcdef"}}

一眼能看出为什么红：行标签是 b 开头那个社区，解析出的是 a 开头那个。四份固定件里另外三份分别是正例 good.jsonl（auth_check 放行 → write_insert → 行标签干净的 read_message_rows）、bad_host_channel_mismatch.jsonl 和 bad_coverage_breach.jsonl。tests/replay_fixtures.rs 的做法是先用 Rust 把 trace 构造一遍、序列化、跟入库文件逐字节比对，再回放判决——模式一改，固定件对不上就必须在同一个 PR 里更新。

顺带一提，tests/proptest_checker.rs 的注释里有个判断也值得单独记下来：它明确拒绝写一个「平行 oracle」去重算判决，因为那只是把检查器抄一遍、拿代码测自己。它转而断言若干条从规范形状读得出来的事实（带外来行标签的读必须红、干净的 trace 必须绿、ImplBug 必须红等等）。这跟站内讲的对手验证是同一个思路：判的人不能是写的人。

五、边界与代价：它明确不管什么

LIMITS.md 整份文件就是干这个的，把「绿灯不等于什么」一条条写在明处，值得逐条对着自己的系统读。

它不是证明。 覆盖率恰好等于跑到的代码路径，不多不少。一条不安全的分支在 CI 里从没执行过，这层就对它一言不发。

覆盖率违约也只在武装过的路径上生效。 新加一个绕过 EmitGuard::arm 的对外端点，整个关口是瞎的。文件里写明这一点靠 code review 保证，不靠这套机制本身。

跨进程泄漏不管。 它只 trace 一个进程。多副本部署下的重放跨节点、分发到错误节点这类问题，只在观察到泄漏的那个副本上留痕。

时序类问题不管。 规范无时间概念，这层也无时间概念。只在高并发或特定顺序下才出现的 bug，除非最终表现成一次 Inv_NonInterference 违规落进 trace，否则不在射程内。

分发扇出不管。 扇出不是规范动作；扇出泄漏会出现在接收方的读/写 trace 里，不在发布方的发射里。

类型围栏不管。 CommunityId 没有 From<Uuid> 这件事由编译器保证。谁哪天给它加上了，生产围栏破了，这层不会吭声。

规范本身错了不管。 检查器重写的就是规范，规范错了两边一起绿。

代价也要算清楚。生产默认绑的是 NoopTracer（crates/buzz-relay/src/state.rs 里那行 tracer: Arc::new(crate::conformance::NoopTracer)），也就是说线上默认没有信号，这层是纯观测、不回灌决策，关掉只损失可观测性、不改变 relay 的判断。但读侧要拿到独立的行标签，就得额外查一次 channels，而且这次发射是每个过滤器跑一遍的，所以 req.rs 用 state.tracer.enabled() 把整段短路掉——注释里特意说明只靠 trace_state 是否为空来门控不够，因为任何格式正确的请求它都是 Some。

还有一件安全上的事必须说明白：JsonlTracer::create 会按调用方给的路径新建文件（存在则截断），之后每条步骤明文追加一行 JSON，每次都 flush。那份文件里有社区 UUID、主机字符串、频道 UUID 和 actor 前缀。里面没有私钥、没有 payload、没有签名，但它仍然是一份拓扑信息，落在跑测试的那台机器的磁盘上；如果你在 CI 里把它当构建产物上传，就要按敏感数据对待。另外，record 里锁中毒时是直接吞掉继续写的，写失败也只是丢一步——系统性的丢失靠 Drop 守卫那条兜底来报。

六、上手与避坑清单

跑起来最省事的三条命令，LIMITS.md 里列全了。 cargo test -p buzz-conformance --lib 跑模式与检查器单测，cargo test -p buzz-conformance --test replay_fixtures 跑固定件回放，cargo test -p buzz-relay --lib conformance:: 跑守卫自测。为什么会踩：只跑第一条会让人以为门是活的，其实关口发射端和固定件都没验；三条一起跑才覆盖判据、样本、发射三段。

别在没读 TRACE_SCHEMA.md 的情况下改 schema。 为什么会踩：SCHEMA_VERSION 与 trace 里的版本号不等时，check_trace 报的是 IllegalTransition，错误消息在讲版本，但变体名会把人带向「转移规则写错了」。怎么避：改字段就在同一个提交里改文档和固定件，replay_fixtures 的逐字节比对本来就是逼你这么做的。

BUZZ_CONFORMANCE_UPDATE=1 不是修红灯的开关。 为什么会踩：它能让固定件按当前代码重新生成，红灯立刻变绿，手很顺。怎么避：只有在你确实有意改了 schema 之后才用它，并且改完要人眼看一遍 diff——固定件是给评审看的证据，不是缓存。

包装 tracer 时一定要转发 enabled()。 为什么会踩：trait 上有默认实现，你不写也能编译。怎么避：照 CountingTracer 那样显式委派内层，并给你的包装器补一个跟 counting_tracer_delegates_enabled_to_inner 同形的测试。

读侧写发射时，别拿查询的过滤条件当行的归属。 为什么会踩：手边最顺的值就是 WHERE 里那个 channel id，写下去测试全绿。怎么避：像 project_row_community 那样取行自己的 channel_id，并且把查不到的情况显式变成违约。查询条件和行归属同源，这道关口就是在自证。

读侧那个 claimed_community: None 是刻意的，别顺手改成已解析社区。 为什么会踩：看到一个 None 字段容易觉得是漏填。怎么避：record_req_authcheck 的文档注释已经解释了——订阅请求的线上协议里根本没有客户端声称的社区，h 过滤器带的是频道 id 不是社区 id；写 None 是为了将来真有人开始读线上社区值时，这个字段必须被填成真值，从而在评审时暴露出来。

想验证某一类红灯，就让它成为 trace 里的第一个错。 为什么会踩：check_trace 是快速失败的，只返回第一个错误。你想测 NonInterference，结果前面一步先撞了 StateMismatch，断言就落空。proptest_checker.rs 的注释专门为此立了规矩，它的每个生成器都保证目标违规排在最前。

别把文档当代码的镜像。 TRACE_SCHEMA.md 的发射端表格里，req.rs 那行标的还是「held back」，LIMITS.md 也写着读侧那一半尚未武装；但 crates/buzz-relay/src/handlers/req.rs 里已经有 record_req_authcheck、record_read_message_rows、record_read_by_id_rows 三处真实调用了。高频迭代的项目里文档滞后于代码很正常，判断现状要以代码为准。

收束：三个自检问题

这套东西能不能搬到你自己的系统上，跟你用不用 TLA+ 关系不大。它真正可复用的是三件事：在决策变成可观测行为的那个位置发射结构化事件；用一个不认识生产代码的判据去判；把「什么都没发射」定义成失败。 前两件很多团队做到了一半，第三件几乎没人做，而没有第三件，前两件就是装饰性日志。

落地前对着这三个问题过一遍：

你的关口在哪？能不能指出一个具体函数，说清楚「租户/权限相关的决策在这里第一次变成对外可见的行为」？
你的判据独立吗？它有没有 import 被判方的任何一个归一化函数、任何一个类型？
关口没发射，你的 CI 会红吗？如果只是样本变少了，那这层就还没开始工作。

想继续读源码，顺序建议是：先 crates/buzz-conformance/LIMITS.md 看清边界，再 src/lib.rs 看模式，然后 src/transitions.rs 看判据，最后 crates/buzz-relay/src/conformance/mod.rs 看发射端怎么把真实决策投影过去。

本篇只讲规范与实现之间那一层运行时检查；判的人不能是写的人这条纪律，站内对手验证讲得更系统；把这类关口固化成长期跑的样本集属于回归测试的范畴；至于失败后重试、同一动作发射两次会不会算两笔，那是重试与幂等在管的事；而把可观测事件设计成机器能判而不只是人能看，可以对着可观察日志一起读。

本篇属于一个把开源多 Agent 通信平台 buzz逐层拆开讲的系列，整体地图见 buzz 是什么：Block 开源的多 Agent 通信平台全景图；沿着这条线往下，还可以看 Block 开源 buzz：多 Agent 通信平台的两处形式化验证和 Block 开源多 Agent 通信平台 buzz：人机共处一张消息网。