用数学证明代码正确：形式化验证入门

可视化演示

展示代码形式化验证的三大方法：霍尔逻辑用{P}S{Q}三元组验证程序、模型检测遍历状态空间验证性质、定理证明从公理出发构建证明树。切换模式查看不同验证流程。

规约与断言

造桥工程开工前，甲方乙方要先签一份合同。合同上写着：甲方保证地基承载力不低于 300 吨；乙方保证桥在满载时最大形变不超过 5 厘米。有了这份合同，后面的一切验收、追责才有依据。在代码世界里，这份合同叫“规约”（Specification），它把模糊的“这函数应该没问题”变成白纸黑字的数学描述。

规约由两部分组成。前条件（Precondition）是调用方在调用函数前必须保证成立的状态，相当于“甲方必须把地基打好”；后条件（Postcondition）是函数执行完后必须保证的性质，相当于“乙方必须保证桥不塌”。代码里还有一种“合同抽检员”叫断言（assert），它像施工过程中的临时承重测试——程序运行到这里，如果断言不成立，立刻报警。

整套合同可以浓缩成一个漂亮的三元组标记法：

这份三元组字符量虽小，却是整个形式化验证世界的“合同模板”。第一份合同签好，接下来我们就要讨论：怎么证明签下的合同真能兑现。

Hoare逻辑

有了合同，还需要一种“验算”的方法。回想中学证明题：已知“若 A 则 B”和“若 B 则 C”，就能推出“若 A 则 C”。Hoare 逻辑干的事类似，只不过把 A、B、C 换成了程序状态，把“则”换成了程序的执行步骤。它把一大段代码拆成一条条小的推理规则，像搭积木一样拼出整个程序的正确性证明。

其中最精妙的是 while 循环的推理规则。循环就像桥上来回跑的巡检车，跑多少圈不确定，但我们关心的是：每一圈跑完，车的状态有没有超出安全边界？只要找到一条“无论跑多少圈都成立”的性质，就能对付循环。这条性质叫循环不变式（Loop Invariant），它必须满足：循环开始前成立，每执行一次循环体后依然成立。

Hoare 逻辑把“验证一条循环”变成“找到并验证一个不变式”。这就好比造桥时不需要模拟每一辆车，只需证明“无论车怎么开，中心线都出不了护栏”。找到好的不变式，是证明中最考验功力的地方。

模型检测

Hoare 逻辑像一位数学家，在纸上推公式；而模型检测像一台“全路况模拟器”。假设桥的每一项关键参数（载重、风速、温度）都有有限的取值，把所有取值组合成一张巨大的状态图，然后让计算机系统地把图里所有路径都走一遍，看看有没有一条路径会走出护栏。这是典型的“大力出奇迹”——用算力换安心。

模型检测的关键在于两点。第一，性质用“时态逻辑”表达：不光说“现在安全”，还要说“任何时刻有请求，最终都会得到应答”。第二，反例路径：一旦发现一条违规的路径，系统会原样输出这条路径，工程师就拿着这条“行车记录仪录像”去修复代码，再也不用靠猜。

一条典型的时态逻辑性质长这样：

合在一起，这条公式说的是：任何时候来了请求，最终一定会有应答。模型检测把所有“请求—应答”的时间线全部枚举一遍，任何一条断链都会被抓出来。它的弱点是状态图太大时计算机累趴下——这就是后文要讲的状态爆炸。

定理证明

模型检测像“全路况扫描”，定理证明则是“结构力学推导”——它不枚举车辆，而是从公理出发，用推理规则一步步推导出“这座桥在数学上必然安全”。这正是数学家的老本行：归纳法。

数学归纳法完美对应程序的循环验证。就像验证一排无限长的桥墩：先证明第一个桥墩是稳的（基础步），再证明“如果第 n 个桥墩稳，那么第 n+1 个也稳”（归纳步），于是整排桥墩都稳了。循环不变式验证用的正是同一套思想。

定理证明在计算机上由证明助手（如 Coq、Isabelle）执行。你负责提出证明策略，证明助手负责检查每一步是否符合逻辑规则，绝不放水。更妙的是“类型论”发现：一个类型正确的程序，本身就等价于一个构造性证明——写代码和写证明，其实是一回事。这就像设计桥的图纸上，每一道结构力学的推导都是桥本身的一部分。

关键工具

现实生活中，验桥团队也分工种：有人操作自动化检测机器人，有人是手算结构力学的老教授，还有人负责全城交通仿真。形式化验证的世界里，对应的就是三件代表性工具。

Dafny 像自动化验桥机器人：你在普通代码里标注前条件、后条件和循环不变式，然后点击运行，Dafny 背后的自动定理证明器会自己把大部分证明推完。它强调“可编程”，适合养在 CI 流水线里，每次提交代码自动验一遍。\\Coq\\ 则更像老教授：它的表达能力更强，能证明非常复杂的性质，但你得手动引导证明过程，效率低却上限高，适合操作系统内核、编译器这类“皇冠上的明珠”。\\TLA+\\ 的视野不在单段代码，而在整个分布式系统——它被用来建模并验证 Raft、Paxos 这类共识协议，相当于“全城交通规划仿真”。

\\工具选型的依据很简单：目标在哪个层次。\\ 验证单个函数，用 Dafny；验证算法库的核心不变量，上 Coq；验证分布式系统协议，请出 TLA+。

TLA+ 的核心是“系统状态如何随时间转移”。它用一个带撇的变量表示“下一时刻的状态”：

在 TLA+ 里，整段系统行为就是一条条这样的状态转移公式的组合。验证器在状态空间里搜索，确认不管怎么转移，关键性质都不会被破坏。选对工具，就成功了一半。

完备性局限

听到这里，你可能想问：既然形式化验证这么强，是不是所有代码都能证明正确？答案是：很遗憾，不能。数学家哥德尔和图灵早就画下了一条边界——有些命题本身就无法被计算或证明。最著名的就是停机问题：不存在一个通用程序，能判断任意程序在任意输入下是否会终止。这就好比不存在一种“万能测桥仪”，能预测所有可能建出来的桥的所有行为。

除了理论边界，还有工程边界：模型检测会遇到状态爆炸——变量稍微多一点，状态图就比宇宙原子还多；定理证明则极度消耗人力，一个复杂证明可能要数学家忙上几年。而且，即便证明通过，它证明的也只是“代码满足规约”，如果规约本身写错了——比如桥的设计蓝图承重就少算了一个零——那证明得再漂亮，桥也会塌。

所以现实中的正确策略是：把形式化验证用在真正要命的代码上（航天、金融、协议、安全关键模块），普通代码用测试和代码评审做常规防守。数学不是银弹，但它是最硬的那颗子弹。

AI 应用场景

Python 演示

# -*- coding: utf-8 -*-"""极小命令式语言的穷举验证器通过穷举所有可能的输入组合, 检查程序是否满足规约(前条件/后条件)。这是模型检测思想的最小演示。"""from itertools import product  def eval_expr(e, env):    """求值整数表达式。表达式是元组, 例如 ('plus',('var','i'),('num',1))"""    op = e[0]    if op == 'num':        return e[1]    if op == 'var':        return env[e[1]]    if op == 'plus':        return eval_expr(e[1], env) + eval_expr(e[2], env)    if op == 'mul':        return eval_expr(e[1], env) * eval_expr(e[2], env)    raise ValueError('unknown expr: ' + op)  def eval_bool(b, env):    """求值布尔条件"""    op = b[0]    if op == 'lt':        return eval_expr(b[1], env) < eval_expr(b[2], env)    if op == 'le':        return eval_expr(b[1], env) <= eval_expr(b[2], env)    if op == 'eq':        return eval_expr(b[1], env) == eval_expr(b[2], env)    if op == 'and':        return eval_bool(b[1], env) and eval_bool(b[2], env)    raise ValueError('unknown bool: ' + op)  def exec_cmd(c, env):    """解释执行一条命令"""    op = c[0]    if op == 'skip':        return    if op == 'assign':        env[c[1]] = eval_expr(c[2], env)    elif op == 'if':        if eval_bool(c[1], env):            exec_cmd(c[2], env)        else:            exec_cmd(c[3], env)    elif op == 'while':        while eval_bool(c[1], env):            exec_cmd(c[2], env)    elif op == 'seq':        exec_cmd(c[1], env)        exec_cmd(c[2], env)    else:        raise ValueError('unknown cmd: ' + op)  def verify(program, univ, pre, post):    """穷举所有输入组合, 满足前条件者必须满足后条件"""    names = list(univ.keys())    domains = list(univ.values())    total = 0    passed = 0    for values in product(*domains):        env = dict(zip(names, values))        if not pre(env):            continue        total += 1        exec_cmd(program, env)        if post(env):            passed += 1        else:            print('counterexample:', values)    return total, passed  if __name__ == '__main__':    # 程序: while i < 5 { sum = sum + i; i = i + 1 }    body = ('seq',            ('assign', 'sum', ('plus', ('var', 'sum'), ('var', 'i'))),            ('assign', 'i', ('plus', ('var', 'i'), ('num', 1))))    prog = ('while', ('lt', ('var', 'i'), ('num', 5)), body)     # 前条件: 无限制; 后条件: sum == i * (i-1) / 2    total, passed = verify(        prog,        {'sum': [0], 'i': list(range(6))},        lambda env: True,        lambda env: env['sum'] == env['i'] * (env['i'] - 1) // 2    )    print('verified:', passed, '/', total, 'cases')

1. for values in product(*domains):笛卡尔积展开所有输入的组合，对应模型检测的“状态空间穷举”。
2. if not pre(env): continue只有满足前条件的输入才进入验证范围。
3. exec_cmd(program, env)在给定输入状态下“真实执行”一遍程序。
4. if post(env): passed += 1执行后检查后条件是否成立。
5. print('counterexample:', values)一旦发现反例立即输出，这就是模型检测里的“反例路径”。

常见误区

面试题