解锁形式化验证新潜力：维塔利克·布特林阐述 AI 带来的安全升级价值

形式化验证是用数学方法严格证明系统是否满足规范的技术，可穷尽所有场景提供无死角正确性保证。维塔利克认为AI能通过自然语言转换、自动化模型检测、神经符号推理等方式，降低形式化验证门槛，提升验证效率，助力区块链等复杂系统实现更高安全性。

维塔利克·布特林表示，人工智能辅助的形式化验证或可强化加密安全，但数学证明仍存在重大局限性。

人工智能与形式化证明能否消除加密漏洞？

维塔利克·布特林认为，人工智能可通过形式化验证提升加密货币的安全性。在最近的一篇博客文章中，他指出，借助人工智能的验证技术有望成为抵御日益复杂的软件攻击的重要保障。

这一概念极具吸引力：人工智能生成或检查代码，而数学证明则确保软件完全按照预期运行。从原理上讲，这种方法有望减少严重的智能合约漏洞、交易所风险以及共识失败。

然而，一个重大局限依然存在。即使人工智能推动了形式化验证的发展，加密系统也难以真正保证软件完全无 bug。现实世界的区块链依赖于诸多假设、硬件组件、外部连接、治理机制以及人为决策，而仅靠数学手段并不能完全规避这些风险。

布特林的构想或可大幅提高加密货币的安全性。不过，它不太可能完全消除出现故障的可能性。

维塔利克·布特林阐述了他关于人工智能辅助形式化验证的主张

什么是形式化验证？

形式化验证涉及以数学方式证明软件在既定参数范围内遵循指定规则。

与其完全依赖人工审核员或测试环境，开发者会创建数学描述，以说明系统应如何运行。随后，专业工具会检查代码是否始终符合这些要求。

例如，经过形式化验证的智能合约可能在数学上证明：

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

简而言之，测试旨在验证代码在选定的几种情况下是否能正确运行。而形式化验证则旨在验证代码在证明所涵盖的任何条件下是否都不会违反规则。

这种技术已广泛应用于航空、国防系统以及其他关键硬件和软件领域。加密开发者正越来越多地将其应用于关键安全组件，因为区块链交易往往不可逆转，且可能涉及巨额资金。

苹果corecrypto的正式验证

布特林为何认为人工智能改变了游戏规则

在2026年5月的文章中，布特林指出，人工智能可能显著降低形式验证的主要缺点之一：其复杂性。

传统的形式化验证可能成本高昂、耗时漫长，且需要专业知识。从业者通常需具备定理证明器、证明系统和数学逻辑方面的高级知识。编写证明有时甚至比开发原始软件本身还要费力。

布特林预计人工智能将简化这一工作流程的某些环节。

他描述了一种场景：开发者使用低级语言编写代码，或借助Lean等以证明为导向的工具，而人工智能则协助生成证明、识别不一致之处，并以更少的手动干预确保代码的正确性。

核心思想是：人工智能不仅可能加速软件开发，还有望助力软件安全属性的数学验证工作。

Buterin将这种做法定位为一种防御性应对措施，以应对人工智能在软件分析领域日益增长的使用。如果恶意行为者能够利用人工智能更快地识别漏洞，那么防御方可能需要更强的数学保障，而不能仅仅依赖传统的代码审查。

以太坊联合创始人维塔利克·布特林

加密平台为何易受软件漏洞影响

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

即使是去中心化金融（DeFi）协议中一个微小的编程错误，也可能导致资产被锁定、生成未经授权的代币，或在几分钟内让攻击者耗尽流动性池。以往的加密货币漏洞事件一再表明，即使经过广泛审查的代码，在遇到意料之外的情况时仍可能失效。

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

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

布特林指出，诸如STARK、ZK-EVM、共识协议和后量子密码学等领域是人工智能辅助验证的有前景候选方向。

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

为什么形式化验证无法保证完全的密码安全

尽管形式化验证前景可观，但它仍存在重要局限性。其主要挑战在于，证明仅能确认模型中明确定义的内容。

如果底层假设不完整、不正确或不切实际，即使经过验证的代码也可能失效。证明的可靠性仅取决于其所基于的规范。

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

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

Buterin还指出，形式化验证可能会忽略‘未建模的假设’及其他未解决的组成部分。

即使经过数学验证的桥接合约，仍可能遇到问题，如果：

• 验证者恶意串通。
• 底层密码学变得脆弱。
• 外部组件表现异常。
• 规范存在逻辑漏洞。

形式化验证可降低与软件相关的风险，但无法消除更广泛的系统性风险。

人工智能带来新挑战

人工智能辅助验证也带来了额外的担忧。大型语言模型能够生成看似令人信服但实际上并不正确的逻辑。专家们持续指出，此类风险包括幻觉、不可靠的证明，以及自然语言描述与形式化规范之间的不匹配。

研究表明，人工智能生成的证明可能难以应对：

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

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

此外，还存在一个更广泛的问题：人工智能辅助的验证工具可能会变得过于复杂，以至于只有少数技术专家才能真正理解或评估它们。这可能与加密系统通常所倡导的透明性和广泛参与相冲突。

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

为什么‘足够安全’比‘完全无漏洞’更重要

加密安全最终可能不再那么注重追求完美，而更侧重于降低重大故障发生的可能性。

形式化验证已能让开发者证明智能合约和协议的重要属性。人工智能有望使这些方法更快、更经济且更易于扩展。

仅此进展就能提升以下领域的安全性：

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

然而，“数学上已证明”绝不能被误解为“不可能出错”。

现实世界中的系统融合了代码、人员、经济激励和治理结构。数学能够强化这一系统中的某个部分，但无法消除所有不确定性来源。

布特林的提议有助于加密货币建立更可靠的基础。但不太可能打造一个完全不受黑客攻击、恶意攻击和系统故障影响的生态系统。

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

以上就是解锁形式化验证新潜力：维塔利克·布特林阐述 AI 带来的安全升级价值的详细内容，更多关于维塔利克：AI助形式化验证的资料请关注脚本之家其它相关文章！