币圈界报道：

AI赋能形式化验证：构建抗攻击型加密基础设施

面对日益严峻的数字安全挑战，以太坊联合创始人Vitalik Buterin提出全新视角：人工智能不仅不会加剧区块链系统的脆弱性，反而可能成为其最坚固的防线。他主张，借助AI辅助的形式化验证，有望从根本上减少因人为疏漏导致的安全隐患。

从繁琐证明到智能协同：开发者角色的重构

传统上，形式化验证依赖人工编写可被机器验证的数学逻辑，过程繁复且门槛极高，限制了其广泛应用。Buterin认为，随着大模型能力的演进，这一局面正在改变——开发者不再需要亲自构造证明，而是可向AI提出目标，由其同步生成代码与对应的形式化陈述，最终仅需确认结论是否契合设计意图。

端到端验证：抵御强敌的终极屏障

当AI具备自主发现深层漏洞的能力时，若所有核心代码均经过严格形式化证明，即便攻击者使用高级工具扫描，也只会面对已被验证无缺陷的系统。这种“已验证即安全”的闭环机制，使系统具备极强的抗攻击韧性。他举例指出，Arklib项目正探索全链路形式化验证的STARK方案，而evm-asm则致力于构建基于RISC-V指令集的低层级EVM，并通过可读参考实现进行逐行比对验证。

模型适配与本地化实践：轻量级工具的崛起

在具体实现层面，Buterin提到Claude与Deepseek 4 Pro已能胜任Lean语言下的证明撰写任务。同时，专为形式化验证优化的开源轻量模型Leanstral表现亮眼，可在本地部署运行，在多项基准测试中超越部分大型通用模型，展现出兼顾性能与隐私的可行性。

现实瓶颈与边界认知：验证不等于万无一失

尽管前景广阔，但Buterin亦坦承当前技术存在局限。包括已验证编译器中仍被发现的漏洞、部分代码未被覆盖导致的隐藏风险，以及形式化规范未能准确反映实际业务需求所引发的语义偏差。他重申，该技术并非替代现有安全流程，而是作为长期趋势下“降低每行代码缺陷率”的关键补充手段。这一判断恰逢行业震荡期：四天内接连发生三起重大攻击事件，跨链桥Echo、THORChain及Verus-Ethereum项目合计损失超1.9亿美元，凸显出对自动化验证机制的迫切需求。