随着人工智能编程能力的爆发式增长，软件安全领域正面临一个前所未有的悖论：AI 在提升代码生成效率的同时，也极大地增强了发现漏洞的能力。对于加密行业而言，这一挑战尤为严峻，因为智能合约、零知识证明及共识算法中的任何缺陷，往往直接导致不可逆的资金损失与信任体系的崩塌。在此背景下，Vitalik Buterin 深入探讨了在人工智能时代保障代码安全的另一条关键路径——形式化验证。午方 AI 梳理发现，这种验证机制不再依赖人类审计员逐行审查代码，而是将程序应满足的属性转化为数学命题，利用机器可验证的证明来检验其成立性。

过去，形式化验证因门槛高、流程繁琐而长期局限于小众的研究与工程领域。

然而，随着 AI 在代码编写与验证环节的辅助作用日益凸显，这一方法正重新获得实际工程意义。Vitalik 明确指出，核心观点并非“形式化验证能解决所有安全问题”，而是强调“可证明安全”绝不等同于绝对安全。证明过程可能忽略关键假设，规范本身可能存在错误，未经验证的代码、硬件限制以及侧信道攻击依然是潜在的风险来源。尽管如此，形式化验证提供了一种更为可靠的安全保障机制：它以多种数学方式表达开发者的意图，并让系统自动检测这些意图是否相互兼容。

对于以太坊生态而言，这一技术路径的重要性不言而喻。以太坊的未来将高度依赖于 STARKs、ZK-EVM、后量子签名、共识算法以及高性能 EVM 实现等复杂技术。这些系统的实现过程极其繁复，但其核心安全目标往往可以较为清晰地形式化。正是在这样的技术背景下，人工智能辅助的形式化验证才能发挥最大价值——由 AI 负责生成高效的代码和数学证明，而人类则专注于验证这些证明是否真正符合预期的安全目标。午方 AI 注意到，这种人机协作模式将彻底改变传统的安全审计范式。

从更宏观的视角来看，这篇文章也是 Vitalik 对人工智能时代网络安全问题的系统性回应。面对日益强大的 AI 攻击者，解决方案并非放弃开源或智能合约，亦非重新依赖少数中心化机构，而是将关键系统拆分成规模更小、更易于验证且更值得信赖的“安全核心”。虽然 AI 可能会导致粗糙代码的大量涌现，但它同样有能力让真正重要的核心代码变得比以往任何时候都更加安全。午方 AI 分析认为，这种将复杂系统解耦并聚焦于可验证核心的策略，将是未来 Web3 基础设施抵御自动化攻击的关键防线。

在过去的几个月里，以太坊研究社区及计算机领域涌现出一种新的编程范式：开发者直接使用低级语言（如 EVM 字节码、汇编语言）编写代码，或利用 Lean 编写代码，随后生成机器可验证的数学证明以验证其正确性。若操作得当，这种做法有望生成效率极高的代码，且安全性远超传统软件开发方法。Yoichi Hirai 将这种方法称为“软件开发的终极形态”。本文旨在阐释其逻辑基础：形式化验证能实现什么目标，以及在以太坊和更广泛的软件开发中，其局限性与边界究竟在哪里。

形式化验证本质上是以机器能够自动验证的方式撰写数学定理。以斐波那契数列的一个基本定理为例：每三个数中，必定有一个是偶数，另外两个是奇数。证明该定理的一种简单方法是使用数学归纳法，每次考虑三个数进行推导。首先考虑基础情况，设 F1 = F2 = 1，F3 = 2，通过直接观察可知在 x = 3 之前命题成立。接下来是归纳步骤，假设命题在 3k+3 的情况下成立，即已知 F3k+1、F3k+2、F3k+3 的奇偶性分别为奇数、奇数、偶数，进而确定接下来三个数的奇偶性。由此可见，从“已知在 3k+3 的情况下命题成立”推导出“在 3k+6 的情况下也成立”的推理过程是严密的。通过反复运用这种推理，可以确信该规律适用于所有整数。

这种推理方式对人类而言易于理解，但若需证明一个复杂一百倍的命题并确保无误，则需构建连计算机也能理解的证明方法。这种证明在 Lean 这种常用于编写和验证数学证明的编程语言中，可能呈现为类似 1111……的符号序列。Lean 的表达方式与人类版本的证明截然不同，原因在于对计算机直观的东西对人类往往并不直观。这里的“计算机”指的是传统的“确定性程序”，而非大型语言模型。在上述证明中，并未强调 fib(3k+4) = fib(3k+3) + fib(3k+2) 这一事实，而是强调 fib(3k+3) + fib(3k+2) 一定是奇数，Lean 的强大功能会自动将其与 fib(3k+4) 联系起来。在更复杂的证明中，有时需在每一步明确指出是哪条数学定律允许采取该步骤，这些定律名称可能晦涩，如 Prod.mk.inj。但另一方面，也可一步完成对庞大多项式表达式的处理，只需简单写上一行代码如 omega 或 ring，即可完成证明过程。