随着人工智能（AI）编程能力飞速提升，软件安全领域正面临一个核心悖论：AI既能高效生成代码，也能高效发现漏洞。对于加密行业和承载巨大价值的智能合约而言，这一挑战尤为严峻——代码缺陷导致的往往不是简单的程序报错，而是不可逆的资产损失与信任崩塌。
以太坊联合创始人Vitalik Buterin（V神）在其最新文章中，深入探讨了应对这一挑战的一条可能路径：形式化验证（Formal Verification）。这是一种将程序应满足的性质表述为数学命题，并通过机器可检查的证明来验证其正确性的方法。在过去，因其高门槛和复杂性，该技术多局限于学术界与特定工程领域；但随着AI辅助能力的崛起，它正获得新的现实意义。
什么是形式化验证？
形式化验证的核心，是撰写能被机器自动检查的数学定理证明。Vitalik以一个简单的斐波那契数列性质为例进行了说明：每三个数中必有一个偶数。人类可以用数学归纳法轻松证明，但要让计算机“信服”，则需要用如Lean这样的证明辅助语言，将推理过程精确编码。
“它看起来和我上面给出的‘人类版’证明很不一样，”Vitalik写道，“这背后有充分理由：对计算机来说直观的东西，和对人类来说直观的东西完全不同。”
这种不直观和繁琐，曾是形式化验证难以普及的主因。但AI的进展正在改变这一局面，使得编写和验证复杂证明变得前所未有地可行。
从数学定理到程序安全
形式化验证的实际价值，在于它能被用于验证计算机程序的正确性，尤其是涉及密码学与金融安全的代码。程序本身就是一个数学对象，证明其按预期运行，就是在证明一个数学定理。
例如，已有研究团队尝试形式化验证加密通信协议Signal的安全性，证明其在特定密码学假设下，能抵御被动攻击者。Vitalik指出，端到端的形式化验证，不仅能证明协议设计的安全，更能证明实际运行代码的安全，极大提升了“无需信任”的程度——用户无需逐行审查所有代码，只需信任已被证明的数学陈述。
AI时代的安全悖论与乐观未来
Vitalik承认，强大的AI漏洞挖掘能力带来了严峻挑战。有人甚至认为，在AI加持的攻击者面前，防守方的非对称优势将不复存在，进而主张放弃智能合约乃至开源模式。
但他对此持乐观态度，认为AI带来的挑战是“过渡性”的。他引用Mozilla的观点称：“缺陷的数量是有限的，而我们正在进入一个终于可以把它们全部找出来的世界。”
形式化验证并非孤立的解决方案，而是加速一个已有趋势的关键催化剂。这个趋势是综合运用类型系统、内存安全语言、更好的软件架构（如沙箱）、改进的测试方法及形式化验证等多种手段，系统性地减少漏洞。
在以太坊生态中的关键应用
Vitalik指出，形式化验证在目标远比具体实现简单的场景中尤其适用，而这正是以太坊下一阶段关键技术（如STARK、ZK-EVM、共识算法、抗量子签名）的共性。
- STARK：实现复杂，但其核心安全属性（证明的有效性等价于哈希安全性或计算正确性）易于形式化定义。已有Arklib等项目致力于构建形式化验证的STARK实现。
- EVM实现：如evm-asm项目旨在直接用RISC-V汇编编写高性能EVM，并证明其与一个为可读性而设计的参考实现等价，兼顾效率与安全。
- 共识算法与智能合约语言：拜占庭容错共识的bug历来常见，形式化验证价值显著。Vyper等智能合约语言也在探索集成形式化验证。
这种“端到端”验证的巨大价值在于，它能捕捉那些在子系统边界处滋生的、人类难以推理的交互型漏洞。
效率与安全的兼得：“软件开发的最终形态”
Vitalik描绘了一个诱人前景：AI辅助的形式化验证，可能让我们“回到未来”。开发者可以让人工智能直接编写高度优化的汇编代码，同时生成证明，验证该代码与一个为可读性而编写的高级语言实现完全等价。
“这样一来，就不再需要一个代码对象同时在可读性和效率之间做平衡，”他写道，“我们会拥有两个彼此分离的对象：一个是汇编实现，它只为效率而优化……另一个是安全主张，或者高级语言实现，它只为可读性而优化。”这正是Yoichi Hirai所称的“软件开发的最终形态”。
并非万能药：形式化验证的局限与边界
Vitalik用相当篇幅提醒，形式化验证并非银弹。所谓“可证明安全”不等于绝对安全，历史上存在多种失败模式：
- 验证范围不全：只验证了部分代码，未验证部分存在关键漏洞。
- 规范定义错误：形式化规范本身未能正确表述真正需要的安全属性。
- 证明假设不成立：证明依赖的假设在实践中可能被违背。
- 硬件与侧信道攻击：如差分功耗分析（DPA）可绕过数学证明的安全模型。
根本原因在于，形式化验证比较的是“程序”与“形式化规范”这两个数学对象，而非直接与“人类意图”比较。人类的意图是复杂且难以完全形式化的黑箱。
核心理念：意图的冗余表达与一致性检查
Vitalik提出了一个更底层的框架：将测试、类型系统和形式化验证视为同一种安全哲学的不同体现——即用多种方式“冗余地”表达开发者的意图，并自动检查这些表达是否一致。
形式化验证将这一理念推向极致。你可以同时写出高效实现和可读实现，并证明二者等价；也可以列出程序应满足的多种数学属性，并验证其全部满足。AI则让生成这些多样的“意图表达”并检查其一致性变得高效。
实践路径：让AI编写，由人类把关
对于大多数开发者，Vitalik的建议并非亲自撰写复杂证明，而是利用AI。开发者可以让AI（如Claude、DeepSeek或专门微调的Leanstral模型）去编写代码和生成证明。
“这项任务的一个好处在于，它本质上是自我验证的，所以你不需要一直盯着它。”他写道。关键在于，人类需要最终审查AI证明的那个数学命题，是否准确对应了想要保障的安全属性。
结论：构建可信的“安全核心”
Vitalik总结道，形式化验证不会解决所有问题，但对于构建一个不依赖信任少数中心化实体的互联网安全模型至关重要。AI与形式化验证是高度互补的技术：AI提升了代码生成规模但可能降低准确性，形式化验证则能将准确性带回甚至超越从前。
未来软件架构可能分化为“不安全边缘组件”和“安全核心”。边缘组件运行在沙箱中，权限受限；安全核心则必须极其可靠，管理最关键资产与数据。
“当涉及安全核心时，我们不会任由有bug的代码不断扩散。我们会积极控制安全核心的规模……相反，我们会把AI带来的全部额外能力，投入到提升安全核心本身的安全性上。”Vitalik相信，在区块链、操作系统内核、关键硬件等安全核心中，形式化验证将助力实现一个“bug不可避免”成为过去式的、更可信的未来。