经过
这不是一起被调查过的事故。它是用来说明规范鸿沟的门。门禁可以被形式化地证明：只允许持有红色许可证的人进入。证明完全正确。现实要求的是：只有经过授权的人才能进入。红色许可证只是一张更顺手的牌子。证明再完美，也在执行假使命。seL4 自己承认：形式验证能证明代码实现了 specification，specification 是否表达了真正需要的行为，是另一件事。
门不在证明的强度上。门在规范写的是不是那件被托付的事。立法写下「须经授权」。实现把授权改写成「持有红证」。验证者证明实现符合那份已经被改写的规范。三步都可以「完成」。完成的是一次假使命。
假使命不是「使命感不够」。它是另一件被执行的目的：看起来仍在做被吩咐的事，绳子已经绑到别处。红许可证是它最干净的形态——不需要崩溃，不需要蓝屏，不需要市场波动。系统按规范工作。规范已经不是托付。传统软件工程把「规范本身对不对」放在自己的边界之外。使命软件工程把这件被放出去的事收回来。
剖析
定义是这一案唯一真正的战场。托付是只有经过授权的人才能进入。禁区必须先于能力，必须不可绕过。红许可证把「授权」改写成一张更顺手的牌子。牌子一旦可发，禁区就不再是禁区，是实现自己颁发的通行证。能力（放行）压过了禁区（须经授权）。使命绑定在定义这一步已经断了。后面的对齐与达成越认真，越是在给假目的打工。
对齐可以全部为真。写下的规范（只认红证）、编出的代码（验红证）、跑着的系统（有证则放行）、世界上发生的（未授权者持证进入），彼此对齐。它们与托付者心里那句「须经授权」不对齐。形式化方法证明的是前一条链。前一条链不自动等于后一句。正确性是符合给定规范。给定规范可以是假使命的说明书。
达成若等于「证明通过、测试通过、审计通过」，红许可证系统是优等生。验收即结束。合同买的是符合规范的实现。规范里已经为未授权的进入留了门。高峰停在证明，证明停在一份被改写的句子上。
人的三个位置在这里被拆开才看得见。立法若写下「须经授权」，实现不得把授权改写成自颁发的牌子。划界若允许例外，例外本身必须被定义、被约束、被记录、被追究——例外不是更顺手的标签。审判必须能盘问：这一次放行走的是哪一条授权、授权是否仍在托付里。把授权做成红证，是把立法权交给了实现。验证者若只负责「代码是否符合文档」，等于在假使命的门口盖章。
方法论 ≡ 原则 ∧ 步骤 ∧ 理性 ∧ 分级 ∧ 制品 ∧ 角色 ∧ 非法推进。红许可证证明：少了「非法推进」这一条，前面六条可以全部齐全。原则仍在，步骤仍在，证明仍在，分级仍在，制品仍在，角色仍在。推进的却是另一件事。方法必须能失败。如果一种方法不能指出「规范已被改写」，它会把假使命做成合格交付。
它也解释为什么「把定义、对齐、达成填成三张检查单」会掏空方法。三张单都可以勾完。勾完的是红许可证，不是托付。思想实验的价值正在于：没有任何崩溃可以帮忙暴露。暴露必须来自对目的本身的盘问。
