正确性证明要区分安全性和活性
永远拒绝写入，也能通过一半检查
账户系统承诺余额不为负，同一扣款身份不生效两次，还要求依赖健康、余额足够时合法的新扣款最终能够完成。实现者把所有扣款都返回 UNAVAILABLE，前两条约束确实不会被破坏。但 UNAVAILABLE 只表示没有完成扣款，不是对象规范允许的余额不足结果；用户永远无法完成本可完成的扣款，所以还不能说系统符合业务要求。
安全性描述“坏事不会发生”，违反时可用一段有限历史指出坏在哪一步：重复扣款、已确认结果被旧版本覆盖、余额变负。活性描述“好事最终会发生”，例如在依赖恢复和调度持续推进的条件下，一个已受理请求最终成功或进入可处理的失败终态。等了十分钟还未完成，可以违反十分钟的服务目标；若没有时间界限，单看这段有限等待却不能证明“以后永远不完成”。
| 命题 | 所需证据 | 单独满足后仍缺什么 |
|---|---|---|
| 同一身份至多产生一次业务扣款 | 身份覆盖所有重放入口，裁决与效果的原子边界，恢复后仍保留的事实 | 一次都不执行也满足，尚未证明会推进 |
| 已提交版本不会被旧执行者覆盖 | 资源端版本守卫及授权、恢复假设 | 可能没有新执行者获得授权，或资源永远不可达 |
| 每个已受理请求最终有可查询终态 | 持久受理、超时/重试推进、公平调度、终态与恢复责任 | 可能通过重复扣款到达成功，尚未证明安全 |
评审要同时写出命题和前提。Alpern 与 Schneider 对安全性/活性的区分帮助分清要证明什么；它不替代某个业务协议的具体证明。
用一个原子扣款转换练习归纳证明
对象规范与 UNKNOWN 历史的权威说明见状态、操作与故障模型。这里换成初始余额 100 的账户，只允许正整数扣款，不补款；状态为余额 b、成功流水集合 L、按请求身份保存参数和结果的 results。这是教学状态机，不是数据库源码。
要证明三条安全不变量：
I1: b >= 0
I2: b = 100 - sum(entry.amount for entry in L)
I3: L 中同一 request_id 至多一条成功流水把 deduct(k, amount) 整体视为一次原子转换，规则如下。
| 输入状态/分支 | 状态变化与响应 | 为什么保留不变量 |
|---|---|---|
| k 已存在，参数相同 | 返回已保存结果，不改 b 或 L | 重试不增加效果，I1/I2/I3 均不变 |
| k 已存在，参数不同 | 参数冲突，不产生效果 | 避免把同一身份解释成另一笔业务 |
| k 不存在，b 小于 amount | 保存不足结果，不改 b 或 L | 不会因重试时状态变化而改写原结果，账本仍相等 |
| k 不存在，b 足够 | 同时扣 b、追加一条 k 的流水、保存成功结果 | 条件保证新 b 非负；账本和余额减同一 amount；此前没有 k，故唯一 |
归纳从初态 b=100、L为空、results为空 开始，三条式子成立。逐个证明上述转换保持它们，便可推出任意有限次模型转换后仍成立。对于两个不同身份各扣 80，先执行的一笔成功、余额变 20；第二笔因余额不足失败；任一身份重试都不会增加流水。
最重要的假设是“同时”。若实现把查重、余额判断、更新余额、写流水拆成互不保护的步骤，就多出了模型没有的中间状态。两个请求都预查到余额 100，再各扣 80，会得到 -60；两个相同身份各扣 10，若都先看到去重记录不存在，也可能各产生一次效果。前一个反例检查余额原子条件，后一个检查业务身份裁决，不能只修其中一个。
实现审查要标出事务提交或其他线性化点，核对输入谓词、唯一约束、事务覆盖范围以及提交后可恢复的记录。不能看到一条原子 UPDATE 就认为整个表格已经成立；也不能用“先查已处理，再调用外部接口”代替原子裁决。
确认点前后分别枚举故障
沿着“接收请求 → 执行转换 → 持久提交 → 返回响应”放置故障点，比从组件名单开始更能发现遗漏。
| 故障位置 | 模型要求 | 反例会长什么样 |
|---|---|---|
| 提交前崩溃 | 未提交修改不成为可见成功，原身份可重新裁决 | 返回了成功，恢复后却没有扣款或结果记录 |
| 提交后、响应前丢回复 | 原身份重试取回原结果，不再次产生效果 | 客户端把超时当失败，换身份再次扣款 |
| 持久提交后重启 | 保留业务效果与裁决记录之间的关系 | 余额保留、内存去重表丢失，重放再次扣款 |
| 旧执行者暂停后恢复 | 它的后续写仍须经过资源端有效裁决 | 新执行者已发布结果，旧执行者恢复后覆盖它 |
| 灾备恢复或人工重放 | 操作身份和去重事实覆盖实际最长重放窗口 | 去重记录已经过期，历史消息再次生效 |
去重保留期不是随意取一个缓存 TTL。它至少要覆盖客户端重试、消息保留与重投、灾备恢复和人工重放可能带来的最大窗口；若系统允许无限期历史重放，就需要可长期识别的业务唯一事实、归档裁决或明确禁止越界重放，不能承诺一个有限 TTL 能覆盖无限窗口。同一身份的参数也要绑定，避免原金额和重试金额不一致。
旧执行者的完整租约授权、令牌单调性与资源端裁决协议统一见租约和 fencing 令牌，本页只把它列为一项证明义务。合成事故场景是两个分区中的 worker 都认为自己有权处理任务，恢复后的旧 worker 覆盖新结果：故障检测只能产生怀疑，本地租约判断也不等于资源已拒绝旧写，必须核查实际资源所用的守卫和持久状态。
活性要写出环境和调度条件
“不断重试，最终会成功”缺了前提。依赖可以永远失联，毒消息可以每次都失败，队头任务可以挡住后续请求，热点租户也可以一直抢到锁，让另一租户饥饿。CPU 和网络总体繁忙，不能说明每个已受理请求都在前进。
可以把一条可评审的活性命题写成：受理记录已持久保存；所需依赖最终恢复到能完成操作；调用都有本地等待上限；恢复扫描持续运行；每个持续可执行的请求最终获得调度；在这些前提下，请求最终成功，或按明确策略进入带原因和恢复责任的失败终态。终态必须可查询，不能把队列里悄悄删除记录称为“处理完成”。
公平调度也要落到请求：弱公平常指一个持续可执行的动作最终会执行。若某租户只在短暂窗口可执行，而每次都被抢走，弱公平未必足够；应通过配额、轮转、隔离队列或更强的调度条件使承诺成立。有限重试可以把毒消息转入隔离态，但这证明的是“最终得到成功或可处理失败”，不是“每个请求最终都成功”。
对于共识服务，多数节点在线只是部分条件，还需要最终及时的通信、持续调度和正确持久状态，具体见CAP 与共识的边界。Raft 论文分别讨论安全性与进展；FLP 论文说明在完全异步且允许故障的模型中，不能无条件保证确定性共识终止。实际系统通过额外的时间、随机化或故障检测假设争取进展，并非用超时证明对方已死。
安全性不应依赖“旧机器大概不会恢复”这类调度愿望；活性也不能靠关闭版本检查、删除唯一约束来修复。严格拒绝不确定写的方案可能在分区中阻塞；接受待确认意图的方案可以增加接纳，但要付出中间态、积压管理和终态恢复的成本。
从协议保证走到业务保证，中间还有证明义务
| 机制 | 直接保护的范围 | 仍需业务解释的边界 |
|---|---|---|
| 共识日志 | 按协议提交的状态机命令顺序 | 客户端重复命令、读取路径、状态机外部副作用 |
| 数据库事务 | 其覆盖的行和存储域中的原子提交 | 事务外缓存、消息或外部接口不自动同成同败 |
| Broker 确认 | 某产品与配置下的复制、存储或接收事实 | 不是下游业务已经完成，也未必等于所需掉电耐久性 |
| 业务幂等 | 同一业务身份不产生多次被裁决的效果 | 身份覆盖范围、保留期、参数冲突和外部资源是否参与 |
例如 Outbox 方案的证明链可以是：业务状态与待发送记录同事务提交，relay 允许重发，下游在其业务事务内以唯一身份裁决，扫描者能恢复遗漏的唤醒。每一项都需要实现与故障证据，producer.send 成功只覆盖其中一段。跨资源事务、Outbox 与长流程的完整方案保留在跨资源事务与长流程，这里不另维护一套实现教程。
对线性化，证明要找出能解释调用/返回历史的生效点，复制对象还要说明领导权、提交索引和读取协议怎样让它跨节点成立。对最终一致，证明要给出停止新更新、通信恢复及修复公平推进等收敛前提。若用合并结构，常需证明合并满足交换、结合和幂等，并且更新/状态模型满足该结构的要求；CRDT 原始综述没有证明任意“余额不负”约束都能自动分区合并。
RTO/RPO 是恢复目标，不会因写入设计文档而成为保证。实际 RPO 取决于确认、复制、持久化与所用恢复点；RTO 包括检测、授权、容量恢复、校验、客户端重连和用户路径重新可用。服务进程重新健康也可能仍有账务待修复，应分别测量。跨系统恢复方案与测量边界见故障域、RTO/RPO 和切换。
实验：用反例、有限模型与实机逐层核对
第一步输入初始余额 100、A/B 各扣 80，各身份最多重试一次。列出 AABB、ABAB、ABBA、BAAB、BABA、BBAA 六个线性化顺序，按原子转换表逐步计算。预期每条路径最后余额 20、只有一个成功身份；不足结果和成功结果的重试都不改变账本。再把提交后丢响应加入，预期以原身份恢复后仍只有一次逻辑效果。
第二步改掉一个假设：先分别判断余额，之后无条件扣减。安排 A/B 都先看到 100，预期得到 -60。这是安全性反例。再把实现改成始终拒绝，三条不变量仍成立，但一个本可完成的扣款永远不完成，这是活性缺口。最后安排毒消息一直占队头，观察“重试次数持续增长”和“后续请求能到终态”为什么是两件事。
从仓库根执行已有有限模型：
python3 labs/system-design/model_check.py模型说明与脚本包含上述六种顺序、提交前后失败、同键改金额，以及旧审核轮次、旧版本和删除墓碑。预期输出合法分支检查通过，同时展示余额 -60 的故意错误分支。它把事务当作原子动作，其旧令牌检查也预先假定令牌已正确生成，因此不能证明数据库实现、完整授权发号、任意线程调度或网络分区。需要检查完整旧持有者协议时，使用中间件实验入口中的 fencing 有限事件模型，并回到租约权威篇解释其假设。
第三步是实现对应性检查：把模型转换逐项映射到真实事务谓词、唯一键、提交与恢复顺序，再在隔离数据上安排双会话竞争、提交前后断连、重启及重放。若 SQL 少了余额条件，或外部副作用没有参与裁决，模型仍可通过，真实实现却不符合模型。
本页给出了可计算的模型预期与纸面反例，没有把它们记为已执行的数据库/集群故障实验。模型可以穷举自己限定的小状态空间，故障注入可以覆盖真实组件路径，两者都要说明遗漏：一次压测无报错不是全历史证明，有限事件模型也没有验证无限等待下的活性。形式化建模与实现精化的进一步方法可参考 Specifying Systems。
三轮追问：从成立的命题追到没有覆盖的命题
第一轮：压测一百万次没有重复扣款，可以说“已经证明”吗？ 只能说这些输入和调度下未观察到反例。还要检查业务身份、原子边界、持久化和恢复假设；用最小反例探索没碰到的交错，用归纳或模型论证限定协议，再核对实现对应性。评分看是否既承认实测价值，也明确其不能覆盖所有历史。
第二轮：安全性都成立，某租户任务总也不完成，接下来查什么？ 查该任务是否真正耐久受理、是否持续可执行、重试是否有上限、扫描器是否运行、队头是否被毒消息占住、调度与配额是否让该租户饥饿。给出公平推进或隔离终态的规则，不能只增加线程和无限重试。评分看是否给出具体活性前提和可观察证据。
第三轮：为了十分钟 RTO，能否在切换时绕过旧版本守卫？ 这样可能提高表面恢复速度，却把旧执行者覆盖新状态的安全反例重新放进系统。应验证授权和资源守卫、恢复水位、容量及用户路径，再测恢复时间；若在既定故障下达不到目标，应调整架构或公开降级范围，而非把破坏不变量当作完成恢复。评分看是否连接安全边界、恢复流程与可测目标。
闭卷验收
本页 3 道闭卷题收进了下方自测面板：先回忆，再展开参考答案与评分点，最后给三档自评。