夜雨聆风2026 年 5 月 18 日，以太坊创始人 Vitalik Buterin 在个人博客发表了《形式验证浅探》一文，抛出了一个可能改变整个软件行业未来的判断： 在人工智能的帮助下，我们终于能写出 "绝对不会出错" 的代码了。这种被他称为 "软件开发最终形态" 的技术，正在悄悄颠覆我们过去 50 年写代码的方式。
一、一个俄罗斯天才的"数学洁癖"
先说说作者。Vitalik Buterin，1994年出生于俄罗斯科洛姆纳，6岁随家人移居加拿大。他19岁写下以太坊白皮书，20多岁就站在了全球区块链技术的最中心。但Vitalik最迷人的地方不是他多有钱——据估计他的净资产在4.5亿到7.5亿美元之间波动——而是他身上那种极客式的纯粹。
2026年初，他公开宣布自己几乎完全弃用Google Maps改投OpenStreetMap，把Telegram换成Signal，Gmail换成ProtonMail，还在积极探索本地运行大语言模型。这不是一个 tech bro 在表演隐私焦虑，而是一个真正相信"去中心化能改变世界"的人在身体力行。所以当这样一个人，在2026年5月18日突然写一篇长文谈"形式验证"（Formal Verification），你最好认真听。因为他不是在谈一个抽象学术概念，他是在谈人类如何用数学来对抗即将到来的AI黑客时代。
二、为什么现在？一场正在失控的安全军备竞赛
Vitalik在文章开头讲了一个层层递进的故事，每一层都让人背脊发凉：
第一层：普通软件有bug，很烦人。
第二层：这些bug跑到区块链智能合约里，朝鲜黑客可以自动把你的钱转走，而且没有追索权——因为区块链是不可篡改的。
第三层：现在零知识证明（ZK）越来越流行，如果ZK系统本身被攻破，黑客可以悄无声息地抽走所有资金，你甚至不知道发生了什么，也不知道什么时候发生的。
第四层：再过两年，等 Claude Mythos 这种级别的AI再进化两轮，发现bug的速度会比人类修bug的速度快十倍。
这已经不是"注意网络安全"的温馨提示了，这是整个互联网防御体系可能崩塌的预警。
Vitalik引用了一些圈内人的悲观论调。有人说："要加固一个系统，你花的token得比攻击者花的多。"还有人更绝望："我们整个行业建立在确定性代码之上——写它、测它、发布它、知道它能工作。但现在，在最顶尖的几家AI原生公司里，代码库已经开始变成你'相信'它能工作的东西，概率是多少，你已经说不清了。"
甚至有人提议：干脆放弃开源吧。如果代码公开就等于把武器库钥匙交给攻击者，那闭源是不是更安全？
Vitalik说：不。如果这条路走通了，互联网的赛博朋克精神就死了。整个密码朋克运动的根基信念是：在互联网上，防御者拥有不对称优势。建一座数字城堡（加密、签名、证明）比拆毁它要容易得多。如果我们连这个都守不住，那未来的网络安全就只能靠规模经济、全球追凶，以及在"统治"和"毁灭"之间做二选一。
他不同意这种悲观。他认为AI带来的bug发现挑战是真实的，但只是一个"过渡性挑战"。 等新均衡建立起来，我们会得到比以前更偏向防御方的世界。
这个观点得到了Mozilla的印证。2026年4月，Mozilla用Anthropic的Claude Mythos扫描Firefox，两个月内发现了271个漏洞。Mozilla CTO Bobby Holley写道："防御者终于有机会 decisively 获胜……缺陷是有限的，我们正在进入一个终于可以找到它们全部的世界。"
三、形式验证到底是什么？从斐波那契到Lean
好，情绪铺垫够了。那形式验证到底是什么？
Vitalik举了一个极其朴素的例子：斐波那契数列的奇偶性。1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144……规律很明显：每第三个数是偶数，其余是奇数。
人类怎么证明？数学归纳法。假设第3k+1、3k+2、3k+3项分别是奇、奇、偶，那下一组的三项也能推出来是奇、奇、偶。所以对所有整数成立。
这个证明对人类来说很直观。但如果你要证明一个复杂一百倍的东西，而且要非常非常确定自己没犯错呢？你就需要一个能说服计算机的证明。
这就是Lean的用武之地。Lean是一个专门用来写和验证数学证明的编程语言。上面那个斐波那契定理，在Lean里被表达成一系列严格的规则：先告诉计算机"第1、2、3项确实符合规律"，然后告诉它"如果前一组符合，下一组也必然符合"。计算机会一步步检查每一步推理是否合法，不会跳过任何细节。
在Lean的世界里，你不是在"解释"为什么某个等式成立，而是在告诉计算机："我已经确认这些基本事实，现在请你用内置的推理规则自动验证结论。"更复杂的证明里，你有时候得明确指定每一步用的是什么数学定律，名字可能古怪得像密码。但另一方面，展开一个巨大的多项式表达式，你只需要写一两个关键词，计算机就能自动搞定。
这种反直觉和繁琐，就是形式验证近60年来一直小众的核心原因。但现在，AI正在快速改变这个局面——AI可以帮你写这些枯燥的证明，你只需要检查它证明的是不是你真正想要的。
四、验证程序：从Signal到STARK
数学定理的形式化很酷，但Vitalik真正关心的是验证计算机程序的正确性，尤其是那些涉及密码学和安全的东西。
他举了一个让人眼前一亮的例子：Signal加密通讯协议。Signal号称端到端加密，但你凭什么相信它？一群研究者正在用Lean做这件事。他们证明了一个定理：假设某些密码学假设成立，那么只有持有私钥的人才能读到消息内容。
看不懂那些密密麻麻的数学符号？没关系。简单来说，这个证明的核心逻辑是：如果攻击者能偷看Signal的密钥交换消息并破解出会话密钥，那他同时也破解了一个被全世界密码学家公认为"极难破解"的数学难题。既然那个难题被认为是安全的，Signal对被动攻击也就是安全的。
端到端的形式验证意味着什么？ 你不是在证明"某个协议描述在理论上安全"，而是在证明"用户手机上运行的那几兆字节代码实际上安全"。从用户角度，这大大提高了"无需信任"的程度：你不需要审查整个代码库，只需要审查关于它的被证明的陈述。
Vitalik特别指出，形式验证最适合的场景是**"目标比实现简单得多"**的情况。这在以太坊下一阶段要部署的技术里比比皆是：
STARK（一种零知识证明系统）：实现极其复杂，但核心安全属性很简单——如果你看到一个证明指向某个程序、某个输入、某个输出，那么要么哈希算法被破了，要么这个程序确实算出了这个结果。Arklib项目正在构建完全形式验证的STARK实现。
EVM（以太坊虚拟机）：更野心勃勃的是evm-asm项目——用底层硬件指令直接写一个完整的EVM实现，并形式验证它。每个EVM操作码都被翻译成一串底层指令，比如加法操作要处理256位大整数，在64位处理器上需要拆成4段来做。项目目前已经完成了24个操作码的完整证明，整个代码库没有任何"先欠着以后再证"的地方。
共识算法：拜占庭容错共识 notoriously 容易出bug，现在有团队在Lean中实现和证明共识协议。
智能合约语言：Vyper和Verity也在做形式验证。
这里面的巨大价值在于端到端。最恶心的bug往往不是单个子系统内部的，而是两个子系统交界处的交互bug。人类很难对整个系统做端到端推理，但自动化的规则检查系统可以。
五、效率的"返祖现象"：为什么又写回底层指令了？
evm-asm这个项目还有一个更 radical 的面向：它是直接用底层硬件指令写的。
等等，我们不是从汇编进化到C，再从C进化到Rust、Solidity，就是为了不手写底层指令吗？对，但Vitalik描述了一个"回到未来"的图景：
以前，高级语言和底层指令之间有一个 trade-off：底层指令快但难写难读难维护；高级语言好写好读但有效率损耗。这个trade-off存在的前提是，同一份代码既要给人看，又要给机器跑。
但现在有了AI+形式验证，你可以把这个trade-off拆开：
用户只需要自动验证这个证明一次，从此以后就跑快版本。人类只需要读慢版本。安全性和效率兼得。
Yoichi Hirai——Vitalik在文中致谢的审稿人之一——把这叫作**"软件开发的最终形态"**。
六、但等等，形式验证不是万能药
写到这里，如果Vitalik就此打住，那这篇文章就成了形式验证的软文广告。但他没有。他用了一整节来谈形式验证的局限和失败案例，而且这部分 arguably 比前面的乌托邦更有价值。
他引用了Menezes和Koblitz在2004年对密码学证明的批评：Rabin在1979年提出一个"可证明安全"的加密函数，结果Rivest很快指出，正是那个"额外安全特性"让它在面对"选择密文攻击者"时彻底崩溃。为了让协议更可证明，设计者把它设计得更不"自然"，结果在设计师没考虑到的场景里更容易出问题。
然后是他引用的机器可验证证明的失败案例：
CompCert（一个形式验证的C编译器）：2011年被发现生成的PowerPC代码有bug，16位位移字段溢出，而CompCert的语义描述没有指定这个限制，因为"假设汇编器会捕获越界值"。
CompCert-KVX（2022年）：nand指令被错误打印成and，这个bug只有在编译随机生成的程序时才被发现。
Cryspen的libcrux（2025-2026年）：这是Vitalik文章中最尖锐的例子。Cryspen是一家做"高保证密码学"的公司，他们的libcrux库号称"已经过形式验证"并提供"最高级别的保证"。但安全研究者Nadim Kobeissi在2026年初发现了多个漏洞：
2025年11月，Filippo Valsorda独立报告libcrux-ml-dsa在不同平台产生不同的公钥和签名——同样的种子输入，在Alpine Linux的ARM64上和macOS的Apple Silicon上输出不同。bug在一个未验证的备用实现里。
hpke-rs库有一个32位计数器，在发布版本中会静默回绕到零，导致加密nonce重用。对AES-GCM来说，nonce重用会泄露认证密钥，造成通用伪造。
libcrux-psq的AES-GCM解密路径里，有人在解密结果上直接"拆包"而不是处理错误——一个畸形密文就能让整个进程崩溃。
更讽刺的是，Kobeissi团队在Cryspen声称"已验证"的代码里发现了错误的数学规范和错误的证明标注（一个声称"12位值能放进1位"的引理，因为复制粘贴把1从别的地方带过来了）。而且Cryspen的构建系统默认不检查证明，文档说"是"的时候实际答案是"否"。
Vitalik把这些失败归纳为几类：
然后他抛出了一个哲学层面的暴击：
所谓"可证明正确性"，从根本上不能证明软件（或硬件）是"正确"的。
因为人类理解的"正确"是：东西的行为符合用户对开发者意图的理解。而"安全"是：东西的行为不会以损害用户利益的方式偏离用户预期。
这两者都需要比较一个数学对象和人类的意图或期望。但人类的意图和期望是宇宙中最复杂的数学对象之一——我们连自己真正想要什么常常都搞不清，更别说把它形式化写进计算机了。在能模拟人类大脑之前，没有任何东西能证明这种比较。
七、那形式验证到底在做什么好事？
Vitalik给了一个非常漂亮的重新框架：
测试套件、类型系统、形式验证，本质上都是同一种安全方法的不同的实现：用多种不同的方式冗余地表达你的意图，然后自动检查这些不同的表达是否兼容。
他举了一个Python例子来说明这个逻辑：
假设你要写一个计算斐波那契数列的程序。你可以用三种方式表达你的意图：
运行程序时，系统会检查这三者是否一致：公式算出来的结果和例子对不对得上？类型对不对？类型检查器验证类型兼容。而"例子袋"定义往往比直接显式定义更符合人类直觉。
形式验证把这个方法扩展到了极致：你可以用几乎任意数量的不同冗余方式来表达意图，程序只有在它们全部兼容时才通过验证。你可以指定一个优化实现和一个低效但人类可读的实现，验证它们匹配。你可以让十个朋友各自列出程序应该满足的数学性质，然后检查是否全部通过。
AI在这里的角色不是替代人类思考，而是替代人类写那些枯燥的证明。 Vitalik坦白说：你不可能自己去写那些证明。他贴了一段关于SPHINCS签名变体的复杂证明，然后问读者："你能告诉我这段是什么意思吗？"（答案是：它证明了一个关于哈希阶梯的安全性质，除非有哈希碰撞，否则一个消息的签名需要的某个值一定比另一个消息的签名更高。）
实际上，Claude、DeepSeek 4 Pro都足以胜任这个任务。还有一个叫Leanstral的专门模型（可以在笔记本本地跑），在形式证明的基准测试里表现超过了很多通用大模型。
最妙的是，这个任务天生自带验证机制——你不需要盯着AI写，让它自己跑几个小时就行。最坏的情况是它原地打转没有进展。最后你只需要检查：它证明的陈述，是不是你真正想要的那个。
八、观点逻辑：世界运转规则的一次微妙转向
Vitalik这篇文章的深层逻辑，其实是在回应一个更宏大的问题：在AI时代，"信任"的根基是什么？
传统软件开发的世界里，信任建立在几个脆弱的支柱上：
但AI发现bug的能力正在指数级增长。Mozilla的数据很直观：2025年发现一个高危漏洞还是"红色警报"，2026年AI两个月给你找出271个。旧的信任基础设施正在过载。
Vitalik的答案是：不要把信任建立在"人说了什么"上，把它建立在"数学能检查什么"上。 形式验证不是让你相信代码没有bug——它做不到——而是让你相信，代码的多个独立描述之间是一致的。这是一种冗余共识机制，跟区块链的共识逻辑其实异曲同工。
而且他认为，这不会是一个小众极客的玩具。AI正在消除形式验证最大的瓶颈——写证明的人力成本。当AI能自动写底层指令+自动写证明，形式验证就从"航天级奢侈品"变成了"基础设施级标配"。
这里的世界运转规则是：当验证成本低于攻击成本时，防御方就赢了。 过去几十年，攻击者只需要找到一个漏洞，防御者需要堵住所有漏洞。这种不对称让互联网安全像是一场必输的打地鼠游戏。但如果AI能把所有已知缺陷模式都穷举验证一遍，攻击者就必须去找那些连AI和形式验证都覆盖不到的盲区——而那种盲区的数量，会急剧收缩。
当然，Vitalik足够诚实，没有画一个"绝对安全"的大饼。他反复强调的是：形式验证是趋势加速器，不是银弹。 从1990年到2025年，顶级代码安全技术的bug率已经从每千行1个降到了0.01个。形式验证+AI只是让这个曲线继续往下走，而不是突然跳到零。
九、这篇文章的突出之处和局限
突出点：
局限：
Lean中心主义：文章几乎只谈Lean，但形式验证的世界很大（Coq、Isabelle、TLA+、SMT solver等）。Lean确实在AI时代势头最猛——2026年Lean FRO拿了ACM SIGPLAN软件奖，Mathlib是最大形式化数学库——但只字不提其他工具，可能让非Lean读者觉得门槛更高。
对AI风险的乐观假设：Vitalik假设AI主要会被防御者用来写证明，但同样强大的AI也可以被攻击者用来找漏洞。他引用的Mozilla案例里，Claude Mythos本身就是一把双刃剑——Anthropic甚至不敢公开发布它，只通过Project Glasswing给少数大公司受控访问，因为担心被用来制造零日攻击。
"最终形态"可能言之过早：Yoichi Hirai的"软件开发的最终形态"很抓眼球，但历史上每一次号称"最终形态"的技术（面向对象、函数式、敏捷、DevOps）后来都被证明只是过渡阶段。形式验证+AI可能也不例外。
工程落地的摩擦被低估：evm-asm项目自己README就写着"DO NOT USE THIS PROJECT FOR ANYTHING OF VALUE"，指令语义是"凭感觉生成的"且未经验证。从原型到生产级，中间隔着的是无数个"构建系统默认不检查证明"的Cryspen式陷阱。
但话说回来，考虑到这只是一篇“浅探”而非详尽的技术白皮书，上述“缺失”更多是“如果能有会更好”而不是“严重缺陷”。Vitalik给自己的定位很准确：这是一篇让你“入门理解”的文章，不是一本教科书。
十、结语：数学不会骗你，但人还是会
Vitalik Buterin在2026年写的这篇《形式验证浅析》，本质上是一封写给技术社区的冷静情书。
他爱形式验证，但他更清楚形式验证爱不了他全部。他看到了AI+Lean带来的历史性机会——让软件安全从"信念"变成"可检查的事实"——但他也守住了一条底线：在能模拟人类大脑之前，没有任何数学证明能担保"这就是你想要的"。
这个世界运转的基本规则没变：工具再强大，也替代不了人的判断。形式验证能做的，是把"你的多个独立判断之间是否一致"这件事，从"靠信仰"变成"靠计算"。
对于普通用户来说，这篇文章最实用的启示可能是：你不需要学会写数学证明，但你需要开始要求关键系统提供可验证的陈述。 就像当年SSL证书从"可选"变成"标配"一样，形式验证的兼容性可能很快就会从"加分项"变成"入场券"。
而对于攻击者和防御者的永恒博弈，Vitalik给出了一个值得贴在墙上的判断：
缺陷是有限的，我们正在进入一个终于可以找到它们全部的世界。
是不是真的能找到"全部"？也许不能。但"找全部"这个方向本身，就已经在改变游戏的赔率了。
原文链接：https://vitalik.eth.limo/general/2026/05/18/fv.html)
