2026程序员必学Lean，形式验证真能消灭bug？
内容提要
2026年，形式验证因AI辅助而复兴，Lean语言成为热门。文章回顾1979年论文的批评，指出验证虽进步，但规格说明翻译、全自动验证、验证后防御等挑战犹存。AI提升证明效率，但验证者正确性、社会过程等根本问题未解，验证仅是可靠性拼图之一。
延伸解读
验证的“社会过程”并未消失
1979年论文指出，数学证明的可信度依赖后续的社会过程，而非证明本身。如今，Lean通过缩小可信内核（约5000行代码）并鼓励多独立实现（如Lean4Lean、Rust内核）来回应这一挑战。这实际上是将“社会过程”部分机器化，但社区审查和维护仍是关键。
规格说明的翻译问题依然尖锐
论文的第二个论点——需求到规格说明的翻译会丢失信息——至今未被驳倒。随着AI辅助证明普及，规格说明更多写给AI而非人类，这加剧了翻译问题。若连与人类同事对齐需求都困难，如何保证写给AI的规格说明准确反映真实意图？
验证通过不等于万事大吉
文章强调，验证通过的程序仍可能因规格说明错误或资源限制而失败。AxDafny实验显示，验证通过的程序在Python下运行可能超时，因为Dafny只保证功能正确性，不保证复杂度。因此，验证不能替代测试、监控等防御手段。
验证只是可靠性拼图的一块
1979年论文的最后一个论点与当今验证社区达成共识：验证的单一视角会遮蔽其他可靠性机制，如代码审查、测试、复用成功设计等。de Moura引用Dijkstra的话，测试能发现bug但无法证明无bug，而验证也非万能，两者互补。
Q&A
2026年形式验证和Lean语言为什么突然流行起来？
2026年，形式验证因AI辅助而复兴，Lean语言成为热门。谷歌趋势显示过去两年“形式验证”和“形式方法”的搜索量飙升，各大AI实验室发布能自动生成证明的模型，如Mistral AI的Leanstral、AxDafny在DafnyBench上达到92.7%的验证成功率，OpenAI的Astra模型在10个数学难题上取得突破并附带Lean 4证明证书。
1979年那篇论文的主要论点是什么？
1979年论文《社会过程与定理及程序的证明》提出几个论点：数学证明的可信度依赖于后续的社会过程；规格说明无法完全描述真实需求；全自动验证器极不可能被造出来；验证通过后程序员可能放弃其他防御手段；真实世界系统难以形式化；验证的单一视角忽视了其他可靠性方法。
Lean语言如何解决信任问题？
Lean的创造者Leonardo de Moura指出，你不需要信任整个Lean，只需信任其内核，内核约5000行代码，小到任何人都能自己写一个。已有Lean4Lean内核用Lean本身证明了其相对于Lean语义的正确性，还有用Rust等实现的独立内核，多个独立实现指向同一结果，这本身就是一种社会过程。
规格说明的翻译问题在2026年依然存在吗？
是的，规格说明的翻译问题依然存在。虽然有了更先进的规格说明语言如Quint，但将模糊需求翻译成形式化规格说明的过程仍是非形式化的，信息可能丢失或误解。而且现在规格说明越来越多地写给AI看，如果连和人类同事对齐需求都费劲，写给AI的规格说明更难保证是真正想要的。
AI在自动验证方面取得了哪些进展？
AI在自动验证方面进展显著：AxDafny在DafnyBench上验证了725/782个实例，成功率92.7%；OpenProver整合了LLM驱动的自动定理证明与Lean 4；Mistral AI发布了Leanstral；OpenAI的Astra模型在10个数学问题上取得突破并附带Lean 4证明证书。但真正意义上的全自动验证仍不存在，人类努力仍是必要的。
验证通过的程序是否就万事大吉？
不是。验证通过的程序可能仍有问题：规格说明可能写错，验证器可能有bug，而且验证只保证功能正确性，不保证性能。AxDafny的实验发现，验证通过的程序编译成Python后运行失败，多因资源限制（如超时），而非逻辑错误。因此验证不能替代测试、监控和防御性编程。
形式验证在哪些领域变得不可或缺？
形式验证在安全关键领域变得不可或缺，例如CERN用形式验证做粒子加速器设施的安全关键系统，牛津大学的研究者做CHERIoT-Ibex处理器的形式验证。这些系统出错的代价是设备损坏、数据丢失甚至人身伤害。
验证只是可靠性拼图中的一块，为什么？
因为验证不能解决需求模糊问题，不能替代代码审查和测试。测试能找到验证找不到的问题，如性能问题、用户体验问题。AxDafny在DafnyBench上验证了92.7%的实例，但剩下7.3%为何验证不了，原因未知。验证只是可靠性拼图中的一块，需要与其他方法结合。
