维塔利克：“AI驱动的形式验证有望成为软件开发核心”

以太坊联合创始人维塔利克·布特林近日透露，以太坊社区正在开展一项实验，旨在利用Lean等形式化验证工具，对以太坊虚拟机字节码及RISC-V汇编等低级语言代码的准确性与安全性进行验证。

形式化验证的应用与优势

布特林指出，形式化验证可应用于加密通信协议、共识算法以及以太坊虚拟机实现等核心基础设施的安全检验。在当前人工智能能够自动发现代码漏洞的环境下，这项技术有助于增强防御方的优势。

技术局限与发展展望

但他同时强调，形式化验证并非万能解决方案。未被建模的假设、侧信道攻击以及验证范围之外的模块等因素，仍可能构成潜在风险。布特林预测，未来软件可能围绕少数安全核心架构进行构建，而人工智能将逐步承担代码生成的工作。