Lean和Z3的创造者：形式化验证的痛苦正在消

有了AI，形式化验证的痛苦正在消失。

OpenAI刚用Astra模型，给10个数学难题做出了机器能查的证明。这背后靠的是Lean——一门既能写代码、又能写证明的语言。

测试只能找bug，证明能消灭bug。

普通测试测得再多，也总有漏网之鱼。但Lean能覆盖所有情况，直接证明程序没错。比如数组越界，你得先证明索引不越界，代码才能跑通。

AI把成本从“10倍”降到了接近零。

以前做形式化验证，花的时间是写代码的10倍。最烦的是后期维护，改一行代码可能让一堆证明全崩。现在有了AI，改证明就像改代码一样轻松。同事用AI一周就搞定了zlib库的翻译和关键证明，过去这活儿得干几个月。

Z3负责找错，Lean负责证明。

de Moura还创造了另一个工具Z3。它像全自动黑箱，适合找漏洞，但没法证明漏洞不存在。而且稍微改下条件顺序，它的证明就可能崩。Lean则是一步步交互着来，每一步都清清楚楚，AI也能跟着一步步学。

人只管说目标，AI负责填步骤。

以后人类只要写好“规格说明”——也就是告诉AI你想要什么。具体怎么证明、怎么优化，全交给AI。手写证明不会死，但纯人工的模式会越来越少。

形式化验证不再是专家特权，马上就要变成日常工具了。