资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
维塔利克·布特林：AI辅助的形式化验证或将成为软件的“终极形态”
以太坊联合创始人维塔利克·布特林表示，人工智能与形式化验证的结合可能成为软件开发的“终极形态”，使开发者能够交付高度优化的代码，同时这些代码的正确性具备机器可验证的证明支撑。他在一篇新文章中写道，形式化验证“特别适用于目标远比实现方案简单的情形”，并指出抗量子签名、STARK证明、共识算法以及ZK-EVM是其主要应用领域。
AI与证明构建的新开发范式
布特林的最新观点呼应了其今年二月提出的主张，即如果生态系统能将人工智能带来的效率提升约一半投入到更严格的测试与验证中，AI或许能“帮助实现近乎无缺陷的加密代码成为现实预期”。他同时提醒开发者不应期待AI生成的代码具有魔力，强调“不能假设仅通过单一指令就能迅速获得高安全性版本；在实现过程中必将与各类漏洞及不一致性进行大量周旋”。
与此同时，他列举了AI辅助形式化方法已在实践中生效的例证，提及某协作项目“通过AI编码完成了对STARK安全性所依赖的最复杂定理之一的机器可验证证明”。这一实验预示了未来可能性：AI工具将协助开发者用证明语言描述目标特性，随后自动搜索并验证特定实现方案是否切实满足这些特性。
安全升级而非安全保证
尽管对此充满热情，布特林多次警示，即便在某个层面实现完美的形式化验证，也无法保证整个系统按预期运行。他在新文章中强调“形式化验证并非万能药”，指出要实现真正的端到端验证，开发者需从高层规范到底层实现进行全面验证，“但这并非遥不可及——相关技术已然存在”。
今年早些时候，他将加密安全定义为“最小化用户意图与系统行为间差距”的课题，在另文中论述“绝对安全”不可能实现，因为人类意图本身具有模糊性且难以形式化。因此他主张采取冗余策略——通过模拟验证、多重签名、形式化验证及多客户端实现等组合方案，而非单纯增加操作摩擦。他认为在多数场景下仍可证明具体安全主张，从而“消除超过99%因代码缺陷导致的负面后果”。
布特林主张，AI应当同时用于加速以太坊路线图与提升其安全标准，而非将速度与安全性视为对立目标。他写道：“人们应保持开放心态，接受以太坊路线图可能以远超预期的速度完成、并达到远超预期安全标准的可能性”，同时提醒开发者即便在AI与形式化验证结合的未来，仍需要持续攻克漏洞及边界情况。
