形式化验证与证明助手

形式化验证通过机器检查的数学证明，确立软件符合其规范；证明助手是构建和检查此类证明的工具。

Definition

形式化验证是构建一个严谨的、经机器检查的证明，以表明系统满足形式化规范；证明助手是帮助用户开发此类证明并机械检查其有效性的软件。

Scope

本主题涵盖演绎验证和交互式定理证明：基于类型理论或高阶逻辑的证明助手（如 Coq、Isabelle、Lean 和 Agda），LCF 可信证明方法，命题即类型基础，证明自动化和策略，以及包括编译器和操作系统内核在内的里程碑式已验证成果。

Core questions

• 如何证明并机器检查完全功能正确性？
• 为什么证明助手值得信赖，可信计算基（trusted computing base）是什么？
• Curry-Howard 同构如何连接证明和程序？
• 验证编译器和内核等真实系统需要什么？

Key theories

LCF 可信证明方法

Gordon、Milner 和 Wadsworth 的爱丁堡 LCF 引入了一个小的可信证明内核，所有定理都必须通过它，因此即使复杂的自动化也无法产生不健全的证明。

已验证编译器 (CompCert)

Leroy 的 CompCert 是一个在证明助手中被证明正确的 C 编译器，其机器检查的定理表明生成的代码细化了源程序的语义。

已验证操作系统内核 (seL4)

Klein 及其同事为 seL4 微内核生成了功能正确性的机器检查证明，展示了低级系统软件的端到端验证。

Clinical relevance

机械化验证为关键软件提供了最高的保证，它生产的编译器、内核和加密库具有经过证明的保证，而非基于测试的信心。证明助手也越来越多地用于形式化数学本身。

History

交互式定理证明始于20世纪70年代的爱丁堡 LCF，其 ML 元语言和可信内核塑造了后来的系统。基于类型理论的助手如 Coq 和 Agda，以及高阶逻辑系统如 Isabelle/HOL 在随后的几十年中逐渐成熟，最终产生了里程碑式的已验证成果：CompCert 编译器（2009年）和 seL4 内核（2009年）。

Debates

验证成本与所获保证之间的权衡

构建大型系统的机器检查证明需要巨大的努力，这引发了关于在何种情况下完全验证是合理的，以及在何种情况下轻量级方法就足够，以及多少证明可以自动化的争论。

Key figures

• Robin Milner
• Michael Gordon
• Xavier Leroy
• Gerwin Klein
• Robert Harper

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

什么是证明助手？

证明助手是一种软件，用户可以在其中交互式地构建形式化证明，而系统则机械地检查每一步，因此完成的证明对于一个小的、经过严格审查的内核来说是值得信赖的。

验证程序与测试程序有何不同？

测试检查选定输入上的行为，只能揭示错误的出现，而形式化验证则证明了规范允许的所有输入的正确性，从而确立了指定错误的缺失。