经过
1991 年 2 月 25 日，海湾战争期间，一枚伊拉克「飞毛腿」导弹击中沙特阿拉伯宰赫兰的美军兵营。爱国者导弹拦截系统本应拦截这枚来袭导弹，却因软件时钟累积误差导致目标跟踪失败。二十八名美军士兵死亡。这不是一次「没写对」的事故。代码忠实执行了设计时的假设。假设已经不再成立。
相邻概念必须被拆开。第一章用 Therac-25 说明信任从硬件转到软件。那是一次托付转移：物理互锁被撤掉，剂量交给程序。爱国者导弹拦截系统在宰赫兰错过拦截，不是同一类失败。时钟累积误差让目标跟踪偏离。代码没有背叛设计。它按当时的假设执行了。世界已经不在那个假设里。正确性是有有效期的。
形式化方法可以证明一段程序符合给定规范，这是正确性。它不自动等于这段程序仍在执行托付。规范可以写错，规范可以过期。正确性是必要条件，不是使命。把正确性当使命，是把绳子交给一份已经过期的说明书。
剖析
定义这一步在设计时是清楚的：拦截来袭的飞毛腿，保护兵营。禁区是不得把跟踪窗口对准一个已经漂移的位置。禁区写在设计假设里——时钟精度足以支撑连续运行若干小时。持续开机的时间越过那一截，假设就不再是假设，是一份过期的许可证。使命绑定要求验证覆盖运行中的这一次，而不是覆盖出厂那一次。
对齐失败发生在时间轴上，而不是发生在模块之间。写下的规范、编出的代码、跑着的跟踪循环，彼此对齐。它们与世界上那枚飞毛腿的真实位置不对齐。接口契约可以全部满足。时间把契约的前提抽走了。这比「两边各写各的单位」更难看见：表面上没有任何接口破裂。破裂的是「系统被允许连续运行多久」这一条从未被当作运行时的检查。
达成若等于雷达还在转、拦截程序还在循环，那天系统达成了。它达成的是一份过期的正确性。托付者是兵营里的士兵。软件执行托付。当假设过期，执行越忠实，后果越确定。
人的三个位置在战时被压缩。立法把拦截写成任务。划界本应规定：开机超过某一时长必须重新校准、必须切换、必须停机人工确认。审判本应能在累积误差越过阈值时拒绝继续自动拦截。把士兵留在已经过期的自动循环里，不是让机器承担使命，是让人在最没有干预余地的位置上承担后果。
分级上，这是关键执行级。自主执行不可逆、高影响的拦截决策，要求运行中确认，而不是出厂证明。出厂证明回答「按这份规范，它当时是对的」。运行中确认回答「这一秒，规范的前提还在不在」。少了后一句，高峰停在实验室。
它也钉住方法学的一条边界。方法论必须能失败。如果一份方法只能证明「符合规范」，不能说出「规范的哪一条前提已经过期」，它会把过期的正确性当成完成。假使命可以寄生在方法里：方法越完整，过期的假设越像一份合格证明。
