第16篇实施证据，2026-09-20
当前：实际累计核心前缀重放+BFS已实现，race完整运行及vet通过。以下为实施前研究记录，状态描述以文末实施映射和verification.txt为准。

# 16：协议验证——确定性注入、历史检查与有限状态搜索

日期：2026-09-20。基线 `d68bdc0de55938518523a47fa7d95ee3868144ed`。状态：前置研究；未实现、未运行任何新二进制。唯一修改本文件。蓝图验收为“找出一个故意漏掉持久化或投票约束的最小反例”。不能预填搜索状态数、轨迹长度或运行通过结果。

## 核心结论与既有证据

本篇应分开三种对象：确定性调度器执行具体实现的一条轨迹；历史 checker 判断外部观察能否解释成合法顺序；状态搜索枚举声明模型的可达状态。它们互相补充，但任何一种的 PASS 都不自动升级为整个 Go 核心的正确性证明。

15 的 `examples/distributed-systems/kv15/README.md` 与同名文章 evidence.txt 已只读核对：直接 import 累计 raft、显式队列和 Block 分区，没有真实 socket；恢复是内存 State 映像；历史 checker 最多 8 个逻辑操作、穷举 pending 选入/省略；已经有回复丢失、漏快照去重、错 waiter 和旧读对照。15 还记录一次错误预期：并发 Add 与 Put 原先存在合法顺序，加入真实 Get 观察后才排除该顺序。这说明“变异启用”不是 oracle 已发现错误的证据。

当前唯一实施方案是对实际累计 Go 核心进行受限环境下的原子事件前缀重放与 BFS。每次 Step 及其完整保存确认循环合并为一个动作，不修改正常核心、不另写选举算法；不把搜索扩大为全部 Raft、KV、快照和成员变更的穷举证明。

## 资料登记与交叉核验

| 标题、版本/日期、URL | 支持论断与定位 | 核验状态/边界 |
|---|---|---|
| MIT 6.5840 Spring 2026 [Schedule](https://pdos.csail.mit.edu/6.824/schedule.html)、[Lecture 15: Verification: IronFleet](https://pdos.csail.mit.edu/6.824/notes/l-ironfleet.txt) | 2026-04-09 验证课；讲义开头明确测试不完整、论文证明不是代码证明 | 已读。日程提示未来讲义可能沿用往年，故称网站当前提供的 2026 课程资料 |
| Stanford CS244B Spring 2024 [Schedule](https://www.scs.stanford.edu/24sp-cs244b/sched/) | Raft、FLP 等原始论文研讨结构 | 已读。不能称本篇 BFS 模型是该课作业，也不能杜撰其有与 MIT 相同的验证讲次 |
| Hawblitzel et al., *IronFleet: Proving Practical Distributed Systems Correct*，SOSP 2015，[原论文](https://pdos.csail.mit.edu/6.824/papers/ironfleet.pdf) | §2.5 信任假设，§3/Figure3 高层规格→协议→实现 refinement，§4 安全/活性及公平性 | 已读。IronRSL 活性前提含存活 quorum 的最终同步，不是任意永久分区也响应；本篇不运行其证明 |
| Leslie Lamport, *Specifying Systems*，First Printing，Version 2002-06-18，PDF 重建 2020-03-19，[作者 PDF](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf) | Chapter 8 活性/公平性，Chapter 14 TLC 可达图探索与使用限制 | 已读相关定位。安全性坏前缀和活性无限执行不能混同 |
| TLA+ Toolbox 1.7.1 [TLC Options Page](https://dl.tlapl.us/tlatoolbox/branches/1.7.1/doc/model/tlc-options-page.html) | Checking Mode：默认 BFS 的安全性反例最短；有界 DFS 通常不保证最短；模拟是另一模式 | 本代理与父独立读取。引用固定文档版本，不声称本机已运行 TLC |
| Musuvathi, Park, Chou, Engler, Dill, *CMC: A Pragmatic Approach to Model Checking Real Code*，OSDI 2002，[原论文](https://www.usenix.org/legacy/event/osdi02/tech/full_papers/musuvathi/musuvathi.pdf) | §3.3/Figure3 状态队列与已访问集合；§3.4 状态空间、hash compaction、抽象可能遗漏错误 | 已读。CMC 直接执行 C/C++；本文虽调用 Go 核心，也只搜索声明的受限环境，不能借其标题扩张覆盖范围。只存短 hash 有碰撞风险 |
| Zhou et al., *FoundationDB: A Distributed Unbundled Transactional Key Value Store*，SIGMOD 2021-06，[项目论文](https://www.foundationdb.org/files/fdb-paper.pdf) | §4、PDF p8：网络、磁盘、时间和伪随机均被抽象，在单进程离散事件模拟中运行多个服务器 | 已读。固定 seed 只有在非确定性来源都受控时才支持回放；不能把随机测试称作穷举 |
| Sela/Herlihy/Petrank, *Linearizability: A Typo*，arXiv:2105.06737v2，2021-07-29，[修订定义](https://arxiv.org/html/2105.06737) | §4/7：纳入见证的 pending 也须遵守扩展后历史的真实时间边 | 本系列15已实际独立读取并据此实现。16引用既有checker边界，不换回原有误 L2 |

## 反向检索及工具版本限制

实际检索模型检查实现的限制、TLC 模式和作者勘误；读取 [Specifying Systems Errata](https://lamport.azurewebsites.net/tla/errata.pdf) 与 [List of Known Toolbox Problems](https://lamport.azurewebsites.net/tla/toolbox-problems.pdf)。后者封面明确 **2009-11-17**，不能因文件今日仍可访问而说其历史 simulation/liveness 问题仍存在于当前 TLC。没有对本机工具版本进行核验，本篇也不需要安装或执行 TLC。

CMC 原文主动说明 fingerprint 冲突与不恰当抽象会漏检；这是方法限制，不需虚构“论文已被推翻”的勘误。IronFleet 原文也列出可信规格、事件循环与环境假设，不把形式化验证包装成无条件正确。一次猜测的 USENIX CMC URL 不可访问，经会议正式记录定位到上述原始 PDF；这是资料定位修正，不是资料不存在。

父独立核对 TLC 1.7.1 的 BFS 最短安全反例说明；当前架构 wiki 的活性错误轨迹不默认最短可作辅助，正文最小性论断以简单单线程 BFS 推导为主，不把安全反例结论套到活性 lasso。

## 唯一实施方案：实际累计核心的原子事件前缀重放

采用现有 Go 核心逐前缀从初始状态重放，再做 BFS，不克隆 Node 私有结构、不另写选举算法。动作仅为 Timeout、一次协议消息交付、CrashRestart；保存确认在各动作内部完成，不作为额外搜索动作。

有限环境固定三节点空日志、term 0/1，只有节点1和2可各执行一次 Timeout（仅 term0 时），节点3最多一次 CrashRestart。不提交应用命令、不调用复制或读 API；一个核心输入事件连同其所有保存/确认完成被视为原子模型动作，故不探索事件内部崩溃窗口。协议消息交付另作动作，可重排；每个后继通过完整前缀重放产生，必须确认原子保存循环结束再接下一事件。

变异放在存储适配器：节点3的 disk 镜像漏保存 Vote，但向 AdvancePersisted 传回原正确 State 作为虚假确认。核心无法观察此谎言，所以能发出成功投票；重启才暴露 disk 中遗失的 vote。这是**违反存储接口契约的适配器故障**，不是核心 AdvancePersisted 漏校验，也不是操作系统实际丢写实验。正常适配器必须实际保存确认的精确映像。针对该变异找最短反例即可满足“漏持久化或投票约束”验收，无需再为投票规则修改生产核心。

预期可达机制为1凭自己和3的票当选，3重启后忘票，2再凭自己和3的票当选。1、2尚未竞选时若提前收到 term1 请求将不再满足 Timeout 条件，因此搜索必须自己找到合法事件顺序，不能用人工设置term让候选进入同任期。两节点的当选审计应跨任期角色变化保留；要求历史同term唯一leader，比只检查当前role更准确。

去重状态的充分性需要单独审查。至少包含：精确 State/disk、当前 role/term/vote、当前候选已收票 ID 集、消息队列全字段及其顺序（若后继依赖下标）、已执行 Timeout 标记、节点3是否已重启、历史 elected/vote 审计。只有 Status.Votes 的票数不够：{1,3} 和 {1,2} 数量相同，未来重复回复效果不同。每一分支必须有自己的审计与消息容器，不能跨重放累积旧观察。

内部字段可按此受限动作集合逐项说明：pending 在每个边界已全部确认；日志/快照为空；无 Replicate 则复制请求序号与 inflight 不参与变化；固定配置无配置轮次；无 BeginRead 则读状态不参与；当选后初始化的 progress 虽存在，但后续不执行复制，不能据此推广到未来允许 AE 的搜索。若无法给出同 key 状态具有相同未来转移与判定的论证，最稳妥的有限方案是把完整事件前缀也纳入 key，不做跨前缀合并：这退化为有限执行树 BFS，性能较差但不因遗漏隐藏字段丢路径。不能以“看起来足够”换取虚假的完备性。

前缀重放应在相同代码版本、模型参数、变异配置下确定地再现全部 Effects；回放时对每一步 enabled 条件和消息来源逐项检查。最短性仍只是这一**受限环境与原子事件粒度**下的最少动作数。即使调用实际 Go 核心，也没有覆盖日志、持久化中途窗口、任意term、任意节点数或并发内存访问；不能称为整个 Go 核心证明。有限模型穷尽/深度截断/资源UNKNOWN的输出规则保持不变。

## BFS 的最短性、完备性与结果类型

采用 FIFO 队列，初始状态深度 0；枚举所有 enabled 动作，边权都为 1；记录前驱和动作，按首次入队去重。在弹出/生成每一层的状态时检查不变量，因此首次反例没有更短的模型动作路径。需要稳定的节点、消息、动作排序，保证同配置回放输出确定；相同深度可能有多个不同最短反例。

状态键必须完整且精确。可用规范序列化的完整状态作 map key；若哈希加速，也必须保留原状态作碰撞比较。节点 ID 不做对称约简、消息不做未经证明的偏序约简，可以少一些性能优化以使最小性论证透明。不要把剩余 crash 额度、精确票集合或历史当选集合漏出状态键；pending 在原子动作边界必须已清空。

本模型域、竞选次数、故障额度和消息类型均有限；若确实遍历到队列为空且未使用资源截断，只能说“该参数下整个有限可达图未发现指定不变量违反”。若设置最大深度 d，输出 NO_COUNTEREXAMPLE_WITHIN_DEPTH 并报告未展开前沿；若达到状态数/内存/时间预算，则输出 UNKNOWN，不能当 PASS。若找到错误则输出 COUNTEREXAMPLE 与完整可回放轨迹。不要把工具终止、异常或空输入解析失败当成验证成功。

这里的最短是原子动作数，不是最少故障次数、最少网络消息、最少实际时间或最少代码修改。固定轨迹的删除缩减最多得到“在给定删减操作下不可再缩短”，通常只是局部最小；不得称全局最短。若要按故障数优先，应更改权重/搜索算法并重新定义最小性，不在本篇混用。

安全违反有有限坏前缀；活性需要考虑无限执行和公平性。故障持续或消息永不交付时，“一直没有 leader”可符合声明的非同步环境，并不自动证明实现有活性 bug。有限步没发生进展不能作为普遍活性反例；全图搜索活性也需要接受循环、时序性质与公平约束。本篇检查一任期一票与 Election Safety 两个安全断言，不实现活性模型检查。

## 手算下界：理论推导，非运行结果

父代理独立推导，在上述固定模型中，节点1和2各需要一次 Timeout 才能产生两个候选人的 RequestVote；节点3必须分别接收一次请求才会产生两次不同候选人的授票；正常易失 vote 约束只有通过节点3的一次 CrashRestart 才能因变异丢失。因此同任期双投至少需要 `2 Timeout + 2 RequestVote 投递 + 1 CrashRestart = 5` 个原子动作。

若目标是两个不同节点实际触发 elected 观察，则每个候选人在自己的自票之外，还需收到节点3的一条成功 VoteResponse；回复的生成和投递是不同事件。因此双 elected 至少需要再加两次回复投递，即下界为 7。这个推导依赖空初始网络、所有请求来自核心、仅1/2竞选、仅3重启、投票按节点去重、保存包含在输入事件内且不另计步数；改变模型或动作粒度就必须重算。

5 与 7 是相应性质的理论下界，不是已运行得到的反例长度。实现须搜索出可达轨迹、回放复核，并确认没有更短路径，才能报告达到下界的最短反例。两个性质需要分别定位第一次违反的前缀；不能在第5步发现双投后提前结束，就声称已运行观察到第7步双 elected。

## 计划验收与对应图示

1. 正常模型完整穷尽或明确返回预算状态；唯一的漏保存 Vote 适配器变异产生真实可回放反例。回放独立读取事件列表，在每一步检查动作 enabled，重算终态错误；篡改一步应拒绝，不能只打印已缓存结论。
2. 对反例长度 L 再做深度 L-1 的遍历，确认同模型/同变异/同动作规则下无更短反例；这作为 BFS 实现自检，不能替代正确状态键与后继枚举审查。
3. 把搜索得到的节点3重复授票证据单独展示：durable/volatile 两列及崩溃点，明确哪一动作首次违反持久化协议、哪一动作首次违反 Election Safety。漏保存本身不等于已经出现双 leader。
4. 用15已有调度历史说明外部历史检查层，保留其内存恢复与无 socket 边界；16核心前缀回放仍需实际验证，并记录代码版本、环境边界与事件粒度，不能默认已完成。
5. 图建议：实现执行/历史检查/状态搜索的证据层次；状态—动作可达图；BFS 分层与首个坏状态；vote 的易失/持久分叉；两多数经节点3交叉的双 leader 轨迹；安全坏前缀与活性循环对比。图上数字以实际搜索输出为准，不先写预计长度。

待交接：本文件研究完成后即可启动累计核心前缀重放驱动设计；不需要继续扩展论文列表。所有搜索结果、最短长度、运行耗时与代码正确性仍未验证；当前仅做只读资料与代码边界核查，没有执行新二进制。



实施映射及边界：
状态键保留完整观察序列、位集、精确votes、disk、Status、消息多重集合及额度；省略私有字段的逐项论证见verify16/README。消息selector无Granted，Delivered保存实际payload；正常同调度消费自身拒绝票。
变异仅适配器disk丢Vote而虚假成功确认，不修改raft核心；单term空日志，实际搜索双投5步、双当选7步。正常有限闭包两个目标各870状态、862展开。小预算1返回UNKNOWN。统计为实测，不从理论下界生成。
图依据：三层验证图来自IronFleet/CMC及系列15；状态动作/BFS图为本实验环境；disk票分叉来自累计Persist契约；双leader7步图来自broken-election.json；正常/变异payload图来自实际selector重放。第16篇未执行TLC/CMC/IronFleet证明或FoundationDB产品。
反例回放仅验证合法action和实际消息/状态/首次目标违反，不认证文件中的搜索统计或最短性。无活性搜索，不证明完整Raft或KV。