币圈界报道：

AI驱动的形式化验证或将重塑软件开发的未来

以太坊联合创始人维塔利克·布特林在最新文章中指出，人工智能与形式化验证的协同将可能成为软件工程的最终形态，使开发者不仅交付高效代码，更可提供可被机器验证的正确性证明。他特别强调，形式化验证尤其适用于目标明确而实现路径复杂的场景，如抗量子签名、STARK证明、共识机制及ZK-EVM等前沿领域。

智能辅助下的新型开发范式正在形成

这一观点延续了其年初提出的设想：若将人工智能带来的效率增益的一半用于强化测试与验证流程，便有可能让近乎零缺陷的加密代码从理想变为现实。但他同时提醒，不能寄望于仅凭一条指令就获得高安全性的成果；实际开发中仍需面对大量漏洞与逻辑冲突。

已有实例表明该路径具备可行性——某合作项目借助AI完成对支撑STARK安全性的核心定理之一的机器可验证证明。这预示着未来开发者只需用证明语言描述预期功能，系统即可自动搜索并验证实现是否满足这些规范。

安全提升不等于绝对保障

尽管前景广阔，布特林反复强调，即便局部实现完美验证，也无法确保整体系统按预期运行。他明确表示：“形式化验证并非包治百病的灵丹妙药。” 要达成端到端可信，必须从高层规范贯穿至底层实现进行全链条验证，而此类技术当前已具备基础条件。

他早前将加密安全定义为“缩小用户意图与系统行为之间差距”的关键挑战，并指出“绝对安全”难以实现，因人类意图本身存在模糊性且难以完全形式化。因此，他主张采用多重保障策略：结合模拟测试、多重签名、形式化验证与多客户端实现，而非单纯增加操作复杂度。他认为，在多数情况下，仍可有效证明具体安全假设，从而规避超过99%因代码缺陷造成的风险。

布特林认为，人工智能应同时服务于以太坊路线图的加速推进与安全标准的提升，二者不应被对立看待。他呼吁保持开放态度，接受以太坊可能以超预期速度达成并达到前所未有的安全水平。同时提醒，即便在高度自动化验证的未来，仍需持续应对未知漏洞与边界情形。