Vitalik Buterin：AI辅助形式化验证或提升区块链安全水平

以太坊联合创始人Vitalik Buterin在5月18日发布的一篇长文博客中表示，人工智能技术的发展可能使软件漏洞的发现更加迅速，但通过将AI生成的代码与形式化验证相结合，有望构建更可靠的加密系统。

形式化验证是一种利用机器可检查的数学证明来确认软件行为符合预期的技术。尽管该方法已有数十年历史，但近年来人工智能的进步显著提升了其实际应用效率，帮助开发者更高效地编写代码及对应的验证证明。

Buterin认为，这一技术对防范智能合约漏洞、保障去中心化金融协议安全具有重要意义。他特别提到以太坊底层基础设施、零知识证明系统、共识机制以及后量子密码学等领域可能从中受益。

图片来源：CoinDesk

他同时指出，形式化验证并非解决所有安全问题的万能方案。若验证基础假设错误、忽略硬件层面缺陷或未覆盖系统全部组件，仍可能导致安全失效。

Buterin强调，人工智能虽可能带来大量低质量代码，但配合形式化验证可有效提升代码准确性，为网络安全提供新的发展方向。

此外，文章还提及以太坊基金会近期出现多位核心成员离职现象，包括Carl Beek、Julian Ma等人，引发外界对其内部治理结构的关注。

（风险提示：本文内容基于公开信息整理，不构成任何投资建议或决策依据。数字资产市场波动较大，投资者应充分了解相关技术与政策环境，谨慎评估自身风险承受能力。）

本文译自CoinDesk，查看原文