# CompCert：关掉编译器假设

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

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

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

> 关节：证明链上每一截假设都必须被显式关掉，或被显式留下。不能误读成「用了 CompCert 就安全」，也不能误读成编译器形式化只是学术。它示范 seL4 那条条件式保证里，有一截曾经被默认为真的 M 与工具链，可以被做成工业对象。

## 经过

CompCert 是被形式化验证的 C 编译器，也是唯一经机器辅助证明免于误编译的生产级编译器。它在 Coq 中证明：针对 C 语言的一个子集，从源代码到汇编的编译保持语义。传统编译器也可以非常可靠。可靠是工程经验。CompCert 关掉的是另一句话——「正确性证明的最后一截，我们交给编译器厂商」。那一截通常不出现在假设清单上。不出现，不等于不存在。优化可以改写，后端可以改写，链接可以改写。程序级证明若在编译之后不再成立，证明停在源文件上。

把编译器做成可证明的对象，是把工具链拉进可信计算基，又把 TCB 里这一截变成可被检查的。这与「我们用了著名编译器」不是同一件事。著名回答的是身份与市场占有。证明回答的是这一次从 C 到汇编是否保持语义。身份不是行为。边界必须同时写上：它出现过能无警告产生错误代码的缺陷；形式化 C 语义与官方标准曾有小差异。高峰不是无瑕。高峰是把瑕疵放进可以盘问的地方。

高峰必须成链。seL4 的证明停在 C。CompCert 把 C 到汇编这一截接上。汇编到硅、硅到板级、板级到系统，仍有假设。链越长，越能看见还剩哪几截是信念。链越短，越容易把信念写成已经完成的保证。2026 年 3 月，CompCert 已为 ATR 42/72 飞机的新一代多功能计算机（MFC_NG）完成合格审定。形式化验证的编译器，已经进入民航关键系统。传统实践中，为便于合格审定，常常需要关闭几乎所有编译器优化。有了正确性证明之后，可以放心地使用优化，依赖证明而非依赖代码模式的可预测性。进入现场不是学科形成，是工具链被当成适航证据的一部分。证据仍是条件式的：在 CompCert 覆盖的 C 子集里，在被证明的后端里，编译保持语义。子集之外、未被证明的插件、手工改写的汇编，都不在这句话里。


![关掉「编译器正确」这一截假设](https://kos-tl.github.io/cases/fig-c11-pass.png)

## 剖析

定义上，CompCert 定义的不是飞机的托付，是编译这一动作的托付：不得在翻译中改变被允许的行为。禁区是优化不得引入源程序没有的行为。能力是生成可用的机器码。禁区先于能力——这是编译器验证必须坚持的顺序。把「生成更快的代码」写在「保持语义」前面，就是红许可证在工具链上的形态。

对齐上，源语义、中间表示、汇编语义被要求对齐。这是对齐在工具链上的硬形态。它不对齐应用层的托付。用 CompCert 编译一段带红许可证的程序，得到的是语义保持的红许可证。工具链高峰会把假使命编译得很干净。

达成上，一次成功的 CompCert 编译，达成的是这一次翻译保持语义。不是达成航电使命，不是达成内核隔离，不是达成一次清算。适航采用把这一截达成写进更长的证据链。证据链仍要问运行中的这一次：是否仍在子集内，是否仍用被验证的后端，是否有人在编译后补了一段未验证的汇编。

人的位置因此改变。立法进入语言子集与语义。划界进入「哪些优化被允许」。审判进入证明对象与适航审查。飞行员不是验证者。验证者在编译器与适航证据里。这与把操作员按 “P” 继续治疗刚好相反：高峰把人从最不擅长的位置上撤下来，放到规格与证明里。撤下来不是无人负责。负责的是写出子集、维护证明、拒绝偷偷改汇编的那些位置。

对方法的借鉴是成链，不是换编译器徽章。seL4 没有 CompCert，证明停在 C，编译器是假设。有 CompCert，假设少一截。少一截不是没有假设。AWS 把 SMT 跑到每天十的九次方量级，又是另一截：规模与可用性。三截必须分开写。写成「高保证已经完成」，是把链上的三座峰压成一张海报。


![高峰必须成链。工具链保证翻译，不是目的](https://kos-tl.github.io/cases/fig-c11-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/)

上一篇：《seL4：精化可以成为开发本身》　下一篇：《AWS Zelkova：工程可用性决定覆盖率》

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