# 红许可证：实现满足规范，可以完美执行假使命

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

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

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

> 关节：规范鸿沟。不能误读成一次真实事故，也不能误读成「形式化方法无用」。思想实验的用处是把方法里最容易被假装填上的那一截单独钉住：证明链可以完整，绳子已经不在原来的目的上。

## 经过

这不是一起被调查过的事故。它是用来说明规范鸿沟的门。门禁可以被形式化地证明：只允许持有红色许可证的人进入。证明完全正确。现实要求的是：只有经过授权的人才能进入。红色许可证只是一张更顺手的牌子。证明再完美，也在执行假使命。seL4 自己承认：形式验证能证明代码实现了 specification，specification 是否表达了真正需要的行为，是另一件事。

门不在证明的强度上。门在规范写的是不是那件被托付的事。立法写下「须经授权」。实现把授权改写成「持有红证」。验证者证明实现符合那份已经被改写的规范。三步都可以「完成」。完成的是一次假使命。

假使命不是「使命感不够」。它是另一件被执行的目的：看起来仍在做被吩咐的事，绳子已经绑到别处。红许可证是它最干净的形态——不需要崩溃，不需要蓝屏，不需要市场波动。系统按规范工作。规范已经不是托付。传统软件工程把「规范本身对不对」放在自己的边界之外。使命软件工程把这件被放出去的事收回来。


![实现满足规范，可以完美执行假使命](https://kos-tl.github.io/cases/fig-c08-pass.png)

## 剖析

定义是这一案唯一真正的战场。托付是只有经过授权的人才能进入。禁区必须先于能力，必须不可绕过。红许可证把「授权」改写成一张更顺手的牌子。牌子一旦可发，禁区就不再是禁区，是实现自己颁发的通行证。能力（放行）压过了禁区（须经授权）。使命绑定在定义这一步已经断了。后面的对齐与达成越认真，越是在给假目的打工。

对齐可以全部为真。写下的规范（只认红证）、编出的代码（验红证）、跑着的系统（有证则放行）、世界上发生的（未授权者持证进入），彼此对齐。它们与托付者心里那句「须经授权」不对齐。形式化方法证明的是前一条链。前一条链不自动等于后一句。正确性是符合给定规范。给定规范可以是假使命的说明书。

达成若等于「证明通过、测试通过、审计通过」，红许可证系统是优等生。验收即结束。合同买的是符合规范的实现。规范里已经为未授权的进入留了门。高峰停在证明，证明停在一份被改写的句子上。

人的三个位置在这里被拆开才看得见。立法若写下「须经授权」，实现不得把授权改写成自颁发的牌子。划界若允许例外，例外本身必须被定义、被约束、被记录、被追究——例外不是更顺手的标签。审判必须能盘问：这一次放行走的是哪一条授权、授权是否仍在托付里。把授权做成红证，是把立法权交给了实现。验证者若只负责「代码是否符合文档」，等于在假使命的门口盖章。

方法论 ≡ 原则 ∧ 步骤 ∧ 理性 ∧ 分级 ∧ 制品 ∧ 角色 ∧ 非法推进。红许可证证明：少了「非法推进」这一条，前面六条可以全部齐全。原则仍在，步骤仍在，证明仍在，分级仍在，制品仍在，角色仍在。推进的却是另一件事。方法必须能失败。如果一种方法不能指出「规范已被改写」，它会把假使命做成合格交付。

它也解释为什么「把定义、对齐、达成填成三张检查单」会掏空方法。三张单都可以勾完。勾完的是红许可证，不是托付。思想实验的价值正在于：没有任何崩溃可以帮忙暴露。暴露必须来自对目的本身的盘问。


![证明实现满足规范，不是证明仍在执行托付](https://kos-tl.github.io/cases/fig-c08-cut.png)

## 对方法的一针

> 证明实现满足规范，不是证明仍在执行托付。规范本身必须被对着托付盘问，例外必须被当成禁区的缺口而不是功能。形式化方法关掉的是「实现是否符合这句话」。这句话是不是那件被托付的事，要另问。没有这一问，高峰是假高峰。

---

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

详细论证、数据口径与未解清单，见同题专著《向软件使命时代进军》第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/)

上一篇：《XZ Utils：清单回答有什么，后门出在怎么来的》　下一篇：《Palantir：有世界、有行动，缺验证与证据》

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