Vitalik：AI+形式化验证或定义软件未来形态

核心提要：以太坊联合创始人维塔利克·布特林提出，人工智能与形式化验证的融合可能成为软件开发的终极范式。他强调该技术可实现代码正确性的机器可验证，已在STARK、ZK-EVM等领域展现潜力，但同时警示其无法替代系统级冗余设计。

AI驱动的形式化验证或将重塑软件工程范式

以太坊联合创始人维塔利克·布特林指出，人工智能与形式化验证的协同将催生软件开发的新纪元，使开发者能够产出高度优化且具备可机器验证正确性证明的代码。他在最新文章中强调，此类方法特别适用于目标明确而实现路径复杂的场景，并重点提及抗量子签名、STARK证明、共识机制及ZK-EVM作为核心应用场景。

智能辅助下的定理证明正迈向现实

这一构想延续了其二月提出的观点：若将AI带来的效率增益中约半数投入更严格的测试流程，便有望让近乎零缺陷的加密代码成为可达成的现实目标。但他也提醒，不能寄望于仅凭一条指令即获得高安全性成果，实际过程仍需应对大量漏洞与逻辑不一致问题。

已有实践案例表明成效初显——某跨团队协作项目借助AI编码工具，成功完成对支撑STARK安全性的关键复杂定理的机器可验证证明。这预示着未来图景：开发者只需以证明语言描述预期功能，系统即可自动搜索并验证具体实现是否满足这些规范。

验证非万能，系统安全需多层保障

尽管前景广阔，布特林反复强调，即便在局部实现完全形式化验证，也无法确保整体系统行为符合预期。他明确表示“形式化验证并非包治百病的解决方案”，真正的端到端保障必须覆盖从高层规范到底层实现的全链路验证，而这类技术当前已具备可行性。

早前他曾将加密系统的安全本质定义为“缩小用户意图与系统实际行为之间的偏差”。他进一步指出，“绝对安全”难以企及，因人类意图本身常具模糊性且难以完全形式化。因此，他主张采用组合策略——结合模拟测试、多重签名、形式化验证与多客户端实现，而非单纯增加操作负担。他认为，在多数情况下，足以通过严谨论证消除超过99%由代码缺陷引发的风险。

布特林认为，应将人工智能用于加速以太坊演进进程的同时提升其安全基线，而非将其视为速度与安全的对立面。他呼吁保持开放态度，接受以太坊可能以超预期速度推进并达到更高安全标准的可能性，但亦提醒即便在高度自动化验证体系下，仍需持续面对漏洞与边界条件挑战。