Paradigm 推出 Solidus：用自动化研究构建经形式化验证的 Solidity 编译器

智能体可以通过自动化研究循环完成非凡的事情。自动化研究者社区可以通过竞赛取得更大的成就，就像我们在 Paradigm Puzzles 上举办的那些竞赛一样。但我们如何知道它们产出的结果是正确的？

使用像 Lean 这样的语言进行形式化验证，结果证明与自动化研究完美互补。它可以证明智能体的输出正确地解决了所提出的问题，或者证明优化后的程序保留了未优化程序的属性。虽然这些证明的构建极其繁琐，但解决方案与问题本身相同：自动化研究。借助 GPT-5.6 和 Claude Fable 5 等能力日益强大的模型，以及 Aristotle 等专用工具，你可以用 AI 自动化生成 Lean 证明。而且它们允许不受信任的贡献者协作，因为贡献可以被证明是正确的。

我们推出 Solidus：一个协作式自动化研究项目，旨在用 Lean 构建一个经过形式化验证的 Solidity 编译器。我们以两个新的优化谜题启动这个项目：一个用于确定 Solidity 语言的冻结源语义，另一个用于优化编译器已经过验证的后端（同时保留证明）。

Solidus 项目已经包含一个完整的形式化验证后端，可将 Yul（Solidity 编译器使用的中间表示）编译为 EVM，以及一个为 Solidity 新提出的形式化语义。我们计划利用自动化研究来最终确定 Solidity 语义、构建编译器的前端，并优化实现，使其不仅成为最安全的 Solidity 编译器，也成为最高效的编译器。

Solidus 已经是一项重大的自动化研究工程。它总共花费了 超过 1,700 小时（约 10 周）的 Codex /goal 时间，采用超高努力、快速模式（按 API 费率约 150,000 美元）。但我们认为，与向公众开放贡献可能带来的改进相比，这不算什么。

这是一个 pre-alpha 项目。代码尚未经过审计，尚未达到生产就绪状态。而且提交内容很可能会利用形式化验证中的细微漏洞来操纵分数或引入未被发现的问题。但我们希望这些挑战能够对这些漏洞进行压力测试，并为未来更雄心勃勃的项目铺平道路。

为什么要对编译器进行形式化验证？

编译器是现代计算工具链的重要组成部分，但它们是复杂且开放的软件，很难进行穷尽式测试。编译器的形式化验证可以防止编译器缺陷，例如导致 2023 年 7 月超过 5000 万美元智能合约黑客攻击的那个缺陷。它还使单个程序的形式化验证更加容易，因为它让开发者能够证明关于高级结构化语言的陈述，而不是低级字节码。

但也许最重要的是，它让我们能够完全放开自动化研究，去改进像编译器这样受信任的代码库。它可以促进在安全代码库上的更多协作，因为贡献可以附带一份证明，表明其满足所需属性。它还允许对编译器进行极其激进、无需信任的优化。基于 Lean 的项目有可能比普通项目被更激进地自动优化。

什么是 Solidus？

Solidus 是一个计划中的编译器，将 Solidity（最流行的智能合约语言）编译到 EVM，用 Lean 实现。

• Lean 是一种用于形式化验证的语言和证明助手。虽然它最广为人知的是在数学中的应用，但它也是一种强大且日益流行的用于计算机程序形式化验证的语言。我们用 Lean 实现了编译器本身，使其更易于进行形式化验证。

• Solidity 是最流行的智能合约语言，而 EVM（以太坊虚拟机）是最流行的区块链虚拟机（被 Ethereum、Tempo 和 Monad 等链使用）。

Solidus 的后端（从 Solidity 的中间表示 Yul 到 EVM 的编译器）已经构建并经过形式化验证。我们使用了 Nethermind 创建的 Yul 和 EVM 语义的略微修改的分支，并证明我们的编译器生成的每个程序对于所有输入都具有与交给它的 Yul 程序相同的输出（除了 gas 和内存布局等 EVM 特定细节）。我们的语义仅对正在编译的单个合约的状态进行建模，但编译器完全支持外部调用——该证明对所有可能的外部世界都是参数化的，只要它们是确定性的。（此后端类似于 Powdr 团队最近发布的 yul-compiler 项目。）

编译器的前端（从 Solidity 到 Yul）尚未构建，部分原因是 Solidity 不存在形式化语义。为了开始纠正这一点，我们构建了一个 Solidity 的形式化语义，作为编译器的源语言。该语义可能仍存在一些缺口，而 Solidus 挑战的目标之一就是找出这些缺口并加固它。

我们如何构建 Solidus

Solidus 之所以成为可能，仅仅是因为 LLM 现在足够强大，能够承担极其繁重的研究和工程项目。主要贡献者是 GPT-5.6 和 Codex，但我们也在一些最复杂的证明中大量使用了 Harmonic 的 Aristotle，并在一些最后步骤中使用了 Claude Fable 5。

没有人类为 Solidus 阅读或编写过一行代码，但它仍然远非完全自动化的成果。我们认为智能体还不够好，无法通过单个 /goal 循环解决这类任务，尽管我们怀疑它们很快就会足够好——大概在今年年底之前。

一个原因是编译器的规范必须随着证明过程而演变；直到我们深入证明过程之前，我们并不清楚我们能够或将会证明关于编译器的确切陈述是什么。这需要一些人类判断，判断哪些规范编辑是可接受的，哪些会违背编译器的精神。将这种判断外包给智能体往往会导致漂移或奖励黑客行为。

另一个原因是，证明的一些更高层架构需要一些人类的创造力。例如，智能体花了数天时间试图证明源程序和目标程序在具体外部世界可能具有的所有可能状态下都是等价的，直到我们建议转向证明这一主张（更强，但讽刺的是，更容易证明）：无论外部世界如何运作，只要每个程序进行的相同外部调用返回相同的结果，它们就是等价的。

我们已经开源了用于构建编译器后端的 Codex 技能。

Solidus 挑战赛

我们认为挑战赛是组织此类集体自动研究项目的理想方式。我们创建了两个挑战赛作为起点：

规范搜寻：形式化验证中的一个棘手问题是，确保针对问题所证明的规范确实符合期望的行为。Solidity 是一门复杂的语言，除了 solc 编译器之外没有正式规范。

我们编写了 solidity-lean，作为对 Solidity 0.8.35 形式化语义的一次尝试，但我们预计其中仍有许多未被发现的偏差。这个挑战赛允许用户通过发现这些偏差并为其提交概念验证来获得积分。这些偏差会使用 Foundry 自动测试，然后由 AI 智能体审查，智能体会通过向 solidity-lean 仓库合并更改来修复它（或在需要时升级为人工审查）。

编译器优化：由智能体生成的形式化验证代码库的另一个问题是，默认情况下它们可能比普通代码库效率更低。在我们的测试套件上，我们的 Yul 到 EVM 编译器目前生成的程序字节码几乎是 solc 的 3 倍。但自动化研究擅长优化，尤其是在正确性可验证的情况下。

我们创建了一个挑战赛，用于优化 Solidus 编译器的 Yul 到 EVM 后端。提交的方案必须在提升现有编译器性能的同时，证明关于其正确性的相同定理。（请注意，当前编译器仅保证可靠性；完整性和性能目前通过留出测试套件进行启发式验证。）

我们希望这些挑战赛将有助于推进 Solidus 项目，并在未来成为其他富有成效的自动化研究项目的原型！