S-Bus：多代理 LLM 状态协调的自动读取集重建

我们解决了通过 HTTP 共享可变状态的 LLM 代理的并发控制，其中不能修改代理来声明读取集。 S-Bus 是一个 HTTP 中间件，其中心机制是服务器端 DeliveryLog，在提交时根据观察到的 HTTP GET 流量重建每个代理的读取集。它提供的一致性属性——可观察读取隔离（ORI），HTTP 可观察读取投影上的部分因果一致性——可以防止专用分片拓扑中的结构竞争条件。三贡献。 (C1)具有三层机械化证据的DeliveryLog机制：TLAPS证明了ReadSetSoundness和ORICommitSafety（模一打字公理）； N=3 时的详尽 TLC 探索了 20,763,484 个州，零违规； Dafny 提出了 9 个归纳引理。 (C2) 与 PostgreSQL 17 SERIALIZABLE 和 Redis 7 WATCH/MULTI 的经验安全性奇偶校验：884,110 次提交尝试中的 I 类损坏为零（427,308 次处于主动争用状态）。 (C3) ORI 在专用分片工作负载中在语义上是中立的，但在单分片协作写入中是有害的，因为保存会传播并发矛盾。 v2 更新：PH-3 LLM 法官现已针对人类注释者（Zahid Hussain、Mindgigs Peshawar）在 400 个（步骤、分片）对上以严格 kappa=0.93（n=93，96.8% 原始一致性）进行独立验证。 LLM 判断间一致性为 kappa=0.46（边界方差）。代理自我报告超额使用分片使用量从 32%（LLM 判断）到 49%（人类注释者）。 SJ-v4 语义质量标准仍然是单一判断 LLM-only。源代码、形式证明、Harness、注释数据：https://github.com/sajjadanwar0/sbus