别再手写证明了，AI Agent 已经把形式方法最苦的活接走了

别学形式化方法。手工写证明，正是形式化方法 75 年来一直小众的原因。seL4 花了约 20 人年，才证明了 8700 行 C 代码。这部分现在由智能体来做。留给你的是规约，以及知道哪种语言适合这项工作。这就是为什么历史很重要。形式化方法，是用精确的数学语言描述程序或系统必须做什么，然后用工具检查代码或设计是否满足要求。下面是我们如何走到今天，每种语言擅长什么，以及我会从哪里开始。

基础（1947 年至 1979 年）
1947 年：Goldstine 和 von Neumann 在程序流程图上标注“断言框”，说明每个点处成立的条件。
1949 年：Alan Turing 的《检查一个大型例程》用断言证明了一个短程序的正确性。这个想法此后十多年基本无人使用。
1962 年：Carl Adam Petri 的论文提出 Petri 网，用于建模并发系统。
1963 年：John McCarthy，《计算数学理论的基础》。
1966-67 年：Peter Naur 和 Robert Floyd 各自独立展示如何通过在代码点上附加断言来证明程序。
1967 年：N. G. de Bruijn 启动 Automath，这是第一种用于计算机检查数学证明的语言。
1969 年：Tony Hoare 发表 Hoare 逻辑，{P} C {Q}。此后几乎所有契约语言都建立在它之上。
1972 年：Robin Milner 的 Stanford LCF。其在爱丁堡的后继者（1979 年）引入 ML 作为脚本语言，是 Standard ML、OCaml 和 F# 的祖先。
1973 年：Mizar 在波兰启动。形式化数学读起来接近教科书。
1975 年：Dijkstra 的卫式命令和最弱前置条件。
1977 年：Amir Pnueli 将时序逻辑引入程序。Patrick 和 Radhia Cousot 发表抽象解释，这是可靠静态分析器背后的理论。
1978 年：Hoare 的 CSP 用于并发进程。Milner 的 CCS（1980 年）和 pi 演算（1992 年）随后出现。
1970 年代：IBM 维也纳实验室的 VDM。Jean-Raymond Abrial 提出 Z，后来在牛津发展。Boyer 和 Moore 构建了他们的定理证明器。

人们使用的工具（1980 年至 1999 年）
1981-82 年：模型检查，由 Clarke 和 Emerson 以及 Queille 和 Sifakis 各自独立发明。2007 年获图灵奖。
1980 年代：法国的同步语言 Esterel 和 Lustre。Lustre 成为 SCADE，空客用它设计飞控软件。
1984 年：康奈尔大学的 Nuprl。
1985 年：Coquand 和 Huet 的构造演算，Coq 背后的逻辑。
1986 年：Isabelle（Larry Paulson）。
1980 年代末：SPARK，Ada 的一个可证明子集。
1988 年：HOL（Mike Gordon）。
1989 年：Coq 首次公开发布。2025 年更名为 Rocq。
1990 年：基于 BDD 的符号模型检查可处理 10^20 个状态。McMillan 的 SMV 随后出现。
1991 年：SPIN 模型检查器公开（Gerard Holzmann，贝尔实验室）。
1992 年：SRI 的 PVS。牛津和 IBM 因在 IBM 的 CICS 事务系统上使用 Z 而获得女王奖。
1993 年：Metamath，一种简单到只需几百行代码即可检查的证明语言。
1994 年：Lamport 的 TLA。TLA+ 于 1999 年出现。
1994-95 年：Intel 奔腾除法错误使其损失 4.75 亿美元。AMD 使用 ACL2，Kaufmann 和 Moore 的