什么是正式验证，为什么Vitalik Buterin认为AI能提供帮助？

人工智能和形式证明能消除加密漏洞吗？

Vitalik Buterin建议，AI可以通过正式验证提升加密安全性。在最近的一篇博客文章中，他认为人工智能辅助验证可能成为抵御日益复杂软件攻击的重要保障。

这个概念很有说服力：人工智能生成或检查代码，而数学证明则证明软件的行为完全符合预期。原则上，这种方法可以减少严重的智能合约漏洞、交易所漏洞和共识失败。

然而，仍然存在一个重大限制。即使人工智能推动了正式验证，加密系统也无法现实地保证软件完全无漏洞。现实世界的区块链依赖于多种假设、硬件组件、外部连接、治理机制以及单靠数学无法完全保护的人类决策。

Buterin的想法有望显著提升加密安全。这不太可能完全消除失败的可能性。

Vitalik Buterin 阐述了他支持人工智能辅助正式验证的理由

什么是正式验证？

形式验证涉及数学上证明软件在定义参数内遵循指定规则。

开发者不再仅依赖人工审核员或测试环境，而是用数学方式描述系统预期的行为。专用工具随后检查代码是否始终符合这些要求。

例如，一个正式验证的智能合约可能在数学上确定：

• 未经适当授权，资产不得提取。
• 代币的总供应量不能超过固定上限。
• 验证者不能进行未经授权的状态更改。
• 在上述条件下，无法进行特定的攻击向量。

简单来说，测试就是询问代码在特定情况下是否正确工作。形式验证则询问代码是否可以在证明涵盖的任何条件下违反规则。

该技术已被应用于航空、国防系统及其他关键的硬件和软件领域。加密开发者越来越多地将其应用于关键安全组件，因为区块链交易往往不可逆且涉及大量资金。

苹果核心加密的正式验证

布特林为何认为人工智能改变了这一方程

在2026年5月的文章中，Buterin认为人工智能可以显著减少形式验证的主要缺点之一：其复杂性。

传统的形式验证可能既昂贵又耗时，且需要专业技能。从业者通常需要对定理证明器、证明系统和数理逻辑有高级了解。写证明有时比开发原始软件需要更多的努力。

Buterin预计AI将简化这一工作流程的部分内容。

他描述了这样一种情景：开发者用低级语言编写代码，或使用如精益等证明导向的工具，而人工智能则协助生成证明、识别不一致并以更少的人工工作检查正确性。

核心思想是，人工智能不仅可能加速软件开发。它还可以帮助支持软件安全属性的数学验证。

Buterin将这种方法描述为对AI在软件分析中日益增长使用的防御性回应。如果恶意行为者能够更快地利用人工智能识别漏洞，防御者可能需要更强有力的数学保证，而不仅仅是依赖传统的代码审查。

Vitalik Buterin，以太坊联合创始人

为什么加密平台容易出现软件缺陷

传统银行通常可以通过既定流程撤销或追回欺诈转账，但基于区块链的系统通常在交易完成后提供的选项较少。

即使是去中心化金融（DeFi）协议中的一个小程序错误，也可能锁定资产、创建未经授权的代币，或让攻击者在几分钟内掏空流动性池。过去的加密漏洞多次表明，即使是经过广泛审查的代码也可能在意外条件下失败。

形式验证尤为重要，因为许多加密组件遵循严格的数学或逻辑规则：

• 共识机制遵循既定的协议。
• 智能合约执行确定性操作。
• 零知识协议依赖于密码学的正确性。
• 桥接和汇总依赖于可验证的状态变化。

Buterin指出，STARK、ZK-EVM、共识协议和后量子密码学等领域是AI辅助验证的有前景候选者。

这些系统可能非常复杂，单靠人工审核可能无法有效扩展。

你知道吗？ 正式验证长期应用于高保证系统，包括飞机软件、防御系统和核反应堆保护系统，软件故障可能带来严重的现实安全后果。

为什么正式验证无法保证完整的加密安全性

尽管形式验证有其承诺，但存在重要的局限性。主要挑战在于证明只能确认模型中明确定义的内容。

如果底层假设不完整、不正确或不现实，即使是经过验证的代码也可能失败。证明的可靠性取决于其所建立的规范。

例如，经过验证的代码仍可能因以下原因而失败：

• 关于用户行为的错误假设
• 有缺陷的外部数据流
• 硬件漏洞
• 编译器错误
• 侧通道攻击
• 治理干预
• 跨链连接的故障
• 模型范围之外的金融攻击

Buterin还指出，形式验证可能忽略“未建模假设”及其他未被解决的部分。

经过数学验证的桥接合同在以下情况下仍可能遇到问题：

• 验证者是恶意勾结的。
• 底层密码学变得脆弱。
• 外部元件表现出乎意料。
• 规范存在逻辑空白。

正式验证可以降低软件相关风险。它无法消除更广泛的系统性风险。

你知道吗？ 尽管经过多次专业审计，仍有一些智能合约漏洞被利用。审计通常考察可能的攻击路径，而正式验证则试图用数学方法证明在特定假设下整个失败类别是不可能的。

人工智能带来新挑战

人工智能辅助验证也带来了额外的担忧。大型语言模型可以产生看似令人信服但实际上错误的逻辑。专家们持续强调诸如幻觉、不可靠证据以及自然语言描述与形式规范不匹配等风险。

研究表明，AI生成的证明可能在以下方面存在困难：

• 复杂的相互依赖关系
• 代码结构的变更
• 模糊要求
• 长长的推理链
• 开发工具更新

人工智能可能加快验证流程，但无法完全取代熟练的人类监督。

还有一个更广泛的担忧。人工智能辅助验证工具可能变得如此复杂，以至于只有少数技术专家能够有效理解或评估它们。这可能与加密系统通常相关的透明度和广泛参与度相冲突。

你知道吗？AI系统正越来越多地被攻击者和防御者在网络安全领域使用。开发者希望AI能更快验证代码安全，攻击者也可能利用AI工具识别漏洞、自动化漏洞发现部分并大规模分析协议弱点。

为什么“足够安全”比“完全无虫”更重要

加密安全最终可能不再追求完美，而是更注重降低重大故障的可能性。

形式验证已经让开发者能够展示智能合约和协议的重要特性。人工智能可以让这些方法更快、更经济、更易于扩展。

仅此一项进展就能提升以下方面的安全性：

• 钱包应用
• 第二层网络
• 零知识系统
• 稳定币基础设施
• 共识软件
• 后量子密码系统

然而，“数学证明”不应与“无法失败”混淆。

现实世界系统结合了代码、人员、财务激励和治理结构。数学可以加强这一体系的一部分，但无法消除所有不确定性。

Buterin的提议可能帮助加密货币发展更可靠的基础。它不太可能打造一个完全没有黑客攻击和系统故障的生态系统。

人工智能辅助的形式验证可能成为加密安全实践中的宝贵补充，而非解决软件漏洞和更广泛系统性风险的全部方案。