# 案例不是配图

向软件使命时代进军 · 方法经 案-00 / 13

本文独立成篇。作者 陈鹏 · 二〇二六年十月

![封面](https://kos-tl.github.io/cases/cover-c00.png)

已发的十二篇是序。脊-01 起是经。经把方法立成可失败的工作：原则、步骤、理性、分级、制品、角色、非法推进必须同时在。这一辑换器官。案例不是配图，也不是休息周的故事合集。案例是方法在哪一截上失败，或高保证实践把哪一截做成了工业事实。证伪不吓人。表彰不展览。做得到指出「这一步非法」，方法才不是又一张表。

甲稿把案例季平行于方法季，错在这里。平行之后，读者仍可以把任何一篇当成金句，仍然不会判断自己有没有在用这套方法。本案不另开故事季。十二案各自成篇，只剖析一截关节。不新造事故，不新造统计。微信从会话列表进来，通常只看一篇。独立不等于无关节。每一篇回指它证伪或示范的那一截，不要求先读完全部。

> 案例若只用来吓人，会退回檄文。案例若只用来表彰工具，会退回展示。

## 负向九例，钉失败

前九篇指出绳子断在哪里。Therac-25 钉信任转移：取消硬件互锁之后，软件接过了剂量，却没有接过可被盘问的绳子。光大证券钉对齐：资金校验是有的，它绑在成交回报之后；检查在场，不等于检查在位。Knight Capital 钉达成：四十五分钟里系统高度可用，它达成的不是做市托付，是一份被重新激活的旧代码。爱国者宰赫兰钉时效：代码忠实执行了设计时的假设，假设已经过期。火星气候轨道器钉可组合性：两边各自正确，合起来把轨道器送进了大气层。CrowdStrike 钉可信计算基：走进内核的保护软件，本身就是单点。XZ Utils 钉供应链：清单回答有什么，后门出在怎么来的。红许可证钉规范鸿沟：实现满足规范，可以完美执行假使命。Palantir 钉对象与保证的分界：有世界、有行动，缺验证与证据。

九例不是九种行业事故。它们是同一套方法被证伪的九个位置。位置乱了，故事会把方法吃掉。把 Therac 写成程序员的错，把光大写成手滑，把 Knight 写成运维没盯盘，把爱国者写成程序发疯，把轨道器写成单位制笑话，把 CrowdStrike 写成供应商丑闻，把 XZ 写成开源有罪，把红许可证写成形式化无用，把 Palantir 写成缺权限——关节就从方法里滑走，重新变成新闻。


![绳子断在哪里：九个关节](https://kos-tl.github.io/cases/fig-c00-neg.png)

## 正向三例，钉高峰停在哪

后三篇不写成英雄榜。seL4 示范精化可以成为开发本身，同时示范保证是条件式：A ∧ S ∧ I ∧ M ⇒ P。16.0.0 在已验证 AArch32 配置上的缓存崩溃，不推翻证明，它指出假设的边界。CompCert 示范如何关掉「编译器正确」这一截通常不被写出的假设；高峰必须成链，链往下走，假使命仍可被干净地编译。AWS Zelkova 示范工程可用性决定覆盖率：用得上的有限检查，盖过用不上的无穷证明。

三例合起来，才是基础工作的完整教训：深度、成链、普通人能用。任何一例单独拿来当「使命已经做成」，都是假使命的一种精致形态。seL4 没有把飞机绑住。CompCert 没有把目的绑住。Zelkova 没有把云上的业务托付绑住。高峰停在高峰上。使命仍要另绑。


![高峰停在哪一截：精化、成链、用得上](https://kos-tl.github.io/cases/fig-c00-pos.png)

## 怎么读这一辑

每一篇四截。钉子是方法上的失败或高峰，不能只是一句判断。经过只收专著已经写明的事实。剖析对着定义、对齐、达成来写，对着五条构成来写。对方法的一针必须能被指出合法或非法。不能误读成，写在关节里，免得故事把位置换掉。

强度与后果挂钩。内部报表不必按剂量系统的绳子来绑。剂量、间隔、清算、调度，不能按内部报表的仪式来绑。案例里的托付者有名字：患者、乘客、存款人、士兵。软件执行托付，不签发托付。

下一篇从 Therac-25 起。它不是怀旧。它是信任转移的原型：从物理规律转到程序，再转到无人能够盘问。今天面对的不是一台加速器，而是成千上万个潜在的、隐藏的同类问题。

---

知识操作系统是架构主张，不是已经交付的操作系统。使命软件工程学尚没有形成。

详细论证、数据口径与未解清单，见同题专著《向软件使命时代进军》第13稿。

在线阅读：檄文 [kos-tl.github.io](https://kos-tl.github.io/index.html?lang=zh) · 专著 [kos-tl.github.io/book](https://kos-tl.github.io/book/) · 体系图 [kos-tl.github.io/system](https://kos-tl.github.io/system/) · 典型案例 [kos-tl.github.io/cases](https://kos-tl.github.io/cases/)

下一篇：《Therac-25：信任转移的原型》

https://kos-tl.github.io/cases/