币圈界报道：

AI赋能形式化验证：重塑加密系统安全边界

面对日益严峻的智能合约安全挑战，以太坊联合创始人Vitalik Buterin提出新视角：人工智能不仅不会加剧攻击风险，反而可能成为强化加密基础设施防御力的关键工具。他强调，通过引入AI辅助的形式化验证机制，可实现对代码逻辑的数学级严格证明，从而构建更可靠的底层信任。

从人工审查到智能协验：验证范式革新

传统形式化验证依赖开发者手动构造可被机器验证的数学证明，过程复杂且门槛极高，长期未能广泛落地。Buterin指出，随着大模型能力提升，如今开发者可将代码与目标规范输入AI系统，由其自动生成配套证明，再由人类仅需核对结论是否契合预期，极大降低实践成本。

在他设想的理想状态下，当AI具备自主发现深层漏洞的能力时，若所有核心组件均经过端到端形式化验证，即便攻击者使用高阶漏洞挖掘工具，所面对的也将是已知无缺陷的代码集合，从根本上消除“致命单点故障”的可能性。

当前已有多个生态项目探索该路径，如专注实现全链形式化验证的STARK方案库Arklib，以及基于RISC-V架构开发、并以可读参考实现为基准进行逐层校验的evm-asm项目，均在推进低层级虚拟机的可信构建。

适配模型与本地部署：轻量高效方案浮现

针对形式化验证所需的特定语言支持，Buterin提到Claude与Deepseek 4 Pro已能胜任Lean定理证明的生成任务。此外，专为Lean优化的开源轻量模型Leanstral表现尤为突出，可在本地设备运行，并在多项基准测试中超越部分大型通用模型，为去中心化安全协作提供可行技术路径。

现实约束与验证边界：警惕技术幻觉

尽管前景广阔，Buterin亦坦承该方法存在明显短板。历史案例显示，即使编译器经验证仍暴露出严重漏洞；部分代码虽经证明，未覆盖区域却隐藏风险；更有甚者，形式化证明虽成立，但其底层规范与开发者真实意图脱节，导致“正确地错”。

他重申，形式化验证并非万能解药，而是推动“代码缺陷趋近于零”这一长期目标的重要补充手段。近期行业接连遭遇重大损失——四日内三起攻击事件，包括跨链桥Echo被盗逾7600万美元、THORChain损失超千万、Verus-Ethereum桥因验证缺失致1158万美元资产流失——恰恰印证了该技术在关键节点上预防局部失效的巨大价值。