系统设计不变量模型

运行：

实验代码

python3 labs/system-design/model_check.py

Python 3.10+ 标准库即可；不连接数据库、不调用外部接口、不写生产数据。脚本枚举两笔扣减及重试的所有线性化顺序，检查非负余额、流水对账与业务幂等；模拟提交前失败、提交后丢响应、同键不同金额；另检查旧审核版本、旧租约与投影删除墓碑。

包含一个故意错误的反例：两个请求均从旧余额100判断可扣80，再分别扣减，余额变成-60。该反例用于说明业务去重之外仍需要原子余额条件。

U78 新增三组内容中心/综合设计检查：content_publish_pointer（发布指针守卫：同一快照并发只有一个写入者成功、草稿不移动指针、被拒者重读可重试）；content_projection_reorder（乱序+重复事件按 aggregate_version 收敛、审计按 event_id 幂等、墓碑版本拒绝迟到发布复活）；capacity_budgets（λW/实例数/失区容量/积压清理/恢复时长/回源倍数的算术与正文一致）。实跑输出与解释见 evidence/u78-2026-10-25.json。

证据边界

Account.deduct 直接把完整事务当成原子状态迁移，证明的是给定模型中的不变量；它不证明MySQL隔离级别、SQL锁范围、磁盘耐久性、Kafka交付或分布式fencing发号。真实SQL仍需运行积分页给出的双会话与崩溃实验。资源token示例假设令牌已正确单调生成，不能证明发号器本身正确。

训练入口：积分、审核、机审、内容中心。