以太坊联合创始人 Vitalik Buterin 提出了开发一种全新编程语言的设想，可直接编译为 Lean 或 HOL（另一种主流形式化验证工具）。
这一构想旨在弥补当前用户在阅读 AI 生成内容时面临的特定短板。随着人工智能在自动生成大量形式化证明方面越来越高效，产出速度早已远超人工手写。但鲜有人能快速验证这些证明实际上成立的内容。
专为 AI 生成证明“读者”打造的语言
Lean 是一款主流的证明辅助工具，数学家与工程师常用其书写形式化证明，实现逐步由计算机校验。以太坊研究员已经利用 Lean 对加密算法代码及共识逻辑进行验证。尽管证明辅助工具行业已发展近 60 年，但整体仍属于小众领域。
Buterin 在其 推文中指出，关于证明内部步骤，唯一的核心要求就是数学上的正确性，不需要其他条件。读者通常不会关注这些具体实现。相比之下，定义及定理则需要人类去阅读与理解，以准确把握软件能提供哪些安全性与功能性保障。
Buterin 也在 5 月份的 博客中进一步探讨了这一思路。他以数学证明为例，展示了如何证明高效的底层代码能严格对应于另一个更易读的规范版本，实现一次审计双重保障。
此时提出该构想也契合以太坊自身的“重构”进程，这一进展被社区称为 Lean Ethereum 路线图。与此同时，研究人员还在推进正式验证的 ZK-EVM开发，即以零知识证明增强易验证性的 EVM 实现，采用的一致方法论。
AI 生成证明，人类核查主张
目前，大型语言模型已经具备编写可用 Lean 证明的能力。Buterin 点名 Claude 与 DeepSeek 4 Pro 具备该项能力，此外 Leanstral（一款专为 Lean 优化的小模型）同样表现不俗。以 evm-asm 项目为例，这是一套经过形式化验证、且与可读规范严格对应的 EVM 实现。相关能力也在 Buterin 最近发起的 AI 挑战中得到体现，测试者数小时内即可完成解题。
更深一层的背景在于安全防护。安全研究表明，今年已出现更多依赖 AI 辅助的攻击尝试。采用形式化验证的代码，可有效阻断此类新型威胁。更友善的规格语言，可以让开发者跳过繁琐证明，直接聚焦对关键主张的审计，提升安全性与开发效率。
影响不限于以太坊研究圈
Buterin 近期持续在公开场合测试这些新理念。例如，他日前展示了一款基于零知识证明的匿名广告牌。该演示表明，可验证声明正逐步从理论研究走向实际应用场景。同时，研究人员也开始在 Lean 环境下对共识客户端进行形式化验证，以便及早发现程序漏洞。
尽管如此，这一发展路径仍保持一贯思路：将高效代码与可读性声明拆分，再通过证明两者一致性。
目前，这一新型编程语言尚无原型产品，Buterin 也未公开详细语法规范。开发者或许会在未来形成统一标准，也可能最终产生多个彼此不兼容的变体。这一选择将直接影响 AI 自动验证代码落地于生产系统的速度。
