ACL2 — 用纯 Lisp 当数学对象，机器证明工业级硬件正确

是什么

ACL2 是一个给硬件和系统软件做数学证明的定理证明器。名字读作 “A-C-L-2”，全称 A Computational Logic for Applicative Common Lisp——“应用式 Common Lisp 上的可计算逻辑”。

日常类比：核电站验机器人。普通工程师写代码靠跑测试，发现 bug 改一改。芯片厂不能这么干——一颗芯片流片要几亿，1994 年 Pentium FDIV 浮点除法 bug 让 Intel 赔了 4.75 亿美元。从那以后，浮点单元、x86 解码器、加密协处理器都得在流片前用数学证明。ACL2 就是干这个的工具。

(defun fact (n)
  (if (zp n) 1
      (* n (fact (- n 1)))))

(defthm fact-positive
  (implies (natp n) (< 0 (fact n))))

第 1-3 行：定义阶乘（普通 Common Lisp）。第 5-6 行：陈述一个定理”自然数的阶乘 > 0”。ACL2 自动跑归纳证完，不需要人手写证明步骤。

这种”程序就是数学对象，定义和定理混在一起写”是 ACL2 的核心姿态。

为什么重要

不理解 ACL2，下面这些事说不清：

为什么 AMD K5 / K7 / Athlon 浮点单元敢说”FDIV / FSQRT / FMUL 全部 IEEE-754 正确”——除法、平方根、乘加在流片前都被 ACL2 证过
为什么 Centaur Technology（VIA 系 x86 厂商）整颗芯片的 RTL 都用 ACL2 表达，每条指令的语义都能符号执行验证
为什么 Rockwell Collins AAMP7G 拿到了 Common Criteria EAL7（最高级）——分离内核的安全策略全在 ACL2 里证完
为什么 ACL2 和 isabelle-hol-2002 / lean-prover 长期共存——三家路线不同：Isabelle/Coq/Lean 走交互式 + 高阶逻辑偏数学家；ACL2 走自动化 + 一阶逻辑偏硬件工程师

核心要点

ACL2 的设计可拆成 4 个抉择：

抉择 1：纯 Lisp 子集 = 程序即数学

ACL2 的逻辑对象就是没有副作用的 Common Lisp 函数。同一份代码：编译运行，是个普通 Lisp 程序；交给 ACL2 内核，是个数学公式。仿真和证明共用一份语义——这是和 hoare-logic 给命令式程序加断言路线最大的差别。

类比：菜谱不光能照着做菜，还能交给营养师验证”这步打蛋会不会让面糊塌”。同一份菜谱、两种用途。

抉择 2：一阶逻辑 + 强自动化

ACL2 的逻辑是一阶、无量词、等式重写。和 isabelle-hol-2002 的高阶逻辑、Coq/Lean 的依赖类型相比，表达力差——不能写”长度为 n 的列表”这种类型，不能直接量词化函数。

代价换来的是：自动化几乎不需要人手指挥。硬件领域 90% 的引理是”两个位向量算法等价”——用归纳 + 重写 + 算术决策过程能闷头做出来。Z3 之类 SMT 求解器（z3-2008 / nieuwenhuis-dpll-t-2006）擅长有限状态决策，但做不了归纳；ACL2 反过来——能做归纳，不擅长复杂的有限状态搜索。

抉择 3：必须能终止

每个 defun 都得证明终止。用户给一个”测度函数”（measure），说明每次递归调用测度严格变小。

类比：下楼梯。每递归一次必须真的下一级，否则机器拒收——这就堵死了”不小心写出无限循环又当数学定理”的洞。

抉择 4：瀑布（waterfall）证明流程

ACL2 自动化的核心是 6 步瀑布：

简化（simplify，重写）
析构消去（destructor elimination）
交叉施肥（cross-fertilization，让左右两侧互相代入）
一般化（generalization，把表达式抽象成变量）
无关项消除
归纳

跑不下去就回到第 1 步从下一个子目标继续。人介入的方式只有一种：写 :hints 提示该用哪条引理或哪种归纳模式。

实践案例

案例 1：AMD K5 FDIV 证明（1996）

Pentium FDIV bug 之后，AMD 把 K5 的浮点单元规格写成 ACL2 函数，把 RTL 实现也翻译成 ACL2 函数，证两者逐位等价。除法用的是 SRT 算法，乘加遵守 IEEE-754 舍入。整套证明在流片前跑完——这是工业界第一次。

案例 2：Centaur 芯片 RTL 全量符号执行

Centaur 把 Verilog 翻译成 ACL2 表达的位向量函数，再用 GL 框架（基于 BDD 和 SAT）做符号执行——一条 x86 指令的所有可能输入一次跑完，看输出是否符合规格。这种规模下人手写 :hints 不现实，工程师靠的是工具链 + 自动化重写规则的积累。

案例 3：书（books）= 可重用证明库

ACL2 的”书”（book）是一份持久化的定义+定理集合，两遍认证：第一遍正常证，第二遍只重放结果。一个项目可能加载几十本书——位向量、IEEE 浮点、x86 解码——就像引依赖。这一机制让 AMD/Centaur 的硬件证明能跨项目复用，否则每芯片从零开始撑不下去。

案例 4：单线程对象（stobjs）= 可证明又可跑得快

硬件证明经常涉及”几百万位的内存状态”。如果用普通 list 表示，每次更新都是新建——证明能写但执行慢到没法符号仿真。ACL2 引入 stobj：逻辑上当成普通的”读出再放回”的纯函数，实际执行在底层 Lisp 用破坏性更新。两边语义对得上，证明照常进行。这种”两面性”是它能撑工业规模的关键工程细节。

踩过的坑

一阶限制让某些自然写法没法表达：你想说”对所有谓词 P，如果 P 在 0 上成立、且 P n 蕴含 P (n+1)，则 P 对所有 n 成立”——这是高阶量词化。ACL2 用 defun-sk 编码量词，但自动化立刻退化，需要人手挑选见证。
终止证明可能很难：累加器风格的递归（(rev xs acc)）测度不直观；互递归（mutual-recursion）要给所有函数一个共同测度。新人常卡在这里。
guards 和逻辑不同步：你写的程序在逻辑上能被接受（被赋值为某种”安全默认”），但不一定能在原生 Lisp 里高效跑——除非你过 guard verification。早期用户经常搞混”我的函数证明通过了” vs “我的函数能跑”。
瀑布发散时排查地狱：自动化跑不动时，trace 输出动辄几千行子目标。老手也得花数小时找出”哪条重写规则把式子带进了死胡同”——这是 ACL2 的学习曲线主体。
重写规则方向性容易翻车：你证了 (rev (rev xs)) = xs，注册成 rewrite rule，瀑布会把所有 (rev (rev x)) 替成 x。但如果反向写成 xs = (rev (rev xs))，瀑布会无限往复杂方向重写直到爆栈——方向是工程师的责任，不是机器的判断。

适用 vs 不适用场景

适用：

硬件浮点单元、ALU、流水线（AMD/Intel/Centaur 的主战场）
微码、低级机器码、加密协处理器（IBM 4758 / Rockwell AAMP7）
编译器后端的算术正确性（位向量 + 模运算 + IEEE 浮点）

不适用：

需要高阶量词或依赖类型——用 isabelle-hol-2002 / lean-prover / Coq
需要有限状态决策（电路等价性、协议模型检查）——用 SAT/SMT（z3-2008 / nieuwenhuis-dpll-t-2006）和模型检查器
命令式程序的断言推理——用 hoare-logic + Dafny / Frama-C / VeriFast 这条线

历史小故事（可跳过）

1971 Boyer & Moore 在爱丁堡造第一版”纯 Lisp 定理证明器”（PLTP）
1979 Boyer-Moore 出书，系统叫 Nqthm（New Quantifier-free Theorem-prover），有了归纳启发式
1994 Pentium FDIV bug 被外部数学家发现 → 工业界第一次认真把硬件验证当生死线
1990 Kaufmann + Moore 启动 ACL2，把 Nqthm 升级到 Common Lisp 宿主、能撑工业代码量
1996 AMD K5 FDIV 在 ACL2 里证完——硬件正式形式化的元年
2000 Kaufmann-Manolios-Moore 出书，把过去 30 年经验系统写下来
2005 ACM Software System Award 颁给 Boyer/Moore/Kaufmann

学到什么

应用式 Lisp = 数学对象：去掉副作用之后，函数本身就是良定的数学函数，不需要再翻译——这是 ACL2 几十年生产力的基础
表达力 vs 自动化是 trade-off：ACL2 砍掉高阶和量词，换来”硬件证明几乎不要人手指挥”的自动化
证明也能写库：books 让证明像代码一样可以复用、依赖、版本——硬件验证规模化的关键
工业里有的证明工具不是越聪明越好，是越稳越好：ACL2 几十年没大改逻辑，AMD/Centaur 才敢把流片押在它身上

关联

isabelle-hol-2002 —— Isabelle/HOL 走高阶 + 交互式，ACL2 走一阶 + 自动化，互补
z3-2008 —— Z3 处理决策片段，ACL2 处理无界递归 + 归纳，常常搭配
nieuwenhuis-dpll-t-2006 —— DPLL(T) 是 SMT 内核机制，和 ACL2 的瀑布是不同自动化哲学
hoare-logic —— Hoare 给命令式程序断言，ACL2 给函数式程序方程
mccarthy-lisp —— Lisp 是 ACL2 的母语，没有 1960 这块石头就没有这门工具
lean-prover —— Lean 4 走依赖类型，和 ACL2 的”无类型 + 总函数”对比鲜明

反向链接

awodey-warren-2009 —— Awodey-Warren — 把『相等的证明』看成两点之间的路径
certikos-2016 —— CertiKOS — 把整个并发内核拆成 30 多层每层都被 Coq 证过
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
hol-light-2009 —— HOL Light — 不到 500 行 OCaml 写出能证开普勒猜想的证明助手
kami-2017 —— Kami — 在 Coq 里造硬件并自动编译到 Verilog
lean-prover —— Lean 4 — 用 Lean 重写的 Lean，让数学家和程序员共用一种语言
mccarthy-lisp —— McCarthy LISP 1960
nieuwenhuis-dpll-t-2006 —— Nieuwenhuis-Oliveras-Tinelli 2006 — 给 SMT 求解器写一套数学规则书
nuprl-1986 —— Nuprl — 第一个把 Martin-Löf 类型论搬上屏幕的证明助手
vamp-verisoft-2006 —— VAMP — 把一颗有流水线、乱序、浮点和 cache 的处理器从门电路证到指令集
z3-2008 —— Z3 2008 — 把 SMT 工程化到工业默认