AI 中文总结
该研究构建了Lean框架EquiVM，利用前沿LLM以代币为代价，为EVM上23个真实合约生成了可复现的基础精化机器证明，实现了此前技术未达的特性组合，重塑验证框架架构。
AI 中文摘要
将底层可执行代码与其行为的高层描述关联起来，是编程语言研究数十年来的核心问题。从形式化验证编译器到翻译验证器、认证编译器以及携带证明的代码，每种方法都在费力但基础的机械化证明与以牺牲完备性、通用性和增加可信基础为代价的自动化之间做出选择。近来，大语言模型（LLM）已开始改变形式化验证的成本结构，智能体式证明开发如今能够产生此前无法企及规模和速度的机器可检查证明。在本文中，我们评估LLM作为事后的、针对每个制品的证书，生成可执行代码与其高层规范之间精化的基础机器可检查证明的能力。我们在以太坊虚拟机（EVM）的背景下研究这一问题，EVM是在以太坊区块链上执行智能合约的底层虚拟机。我们构建了EquiVM，这是一个在Lean中的基础框架，包含可执行的EVM语义和描述智能合约预期行为的规范语言，且不依赖任何源语言或编译工具链。在EquiVM中，精化针对任意来源的已部署字节码进行表述，与未知代码的交互是语义的一部分，每个证明都是可复现的机器可检查证书，此前没有任何技术能实现这种组合。使用前沿商业LLM，在极少人工指导下对23个真实世界合约进行了端到端证明，其中包括MakerDAO稳定币系统的大部分，每个合约的证明规模最高达1亿代币，耗时达100小时。我们得出结论，如今可以以代币为代价获取基础机械化证明，且这一转变可以重塑验证框架的架构方式。
英文摘要
Relating low-level executable code to a high-level account of its behavior has been a central concern of programming-language research for decades. From formally verified compilers to translation validators, certifying compilers, and proof-carrying code, each approach chooses between laborious but foundational mechanized proofs and automation that costs completeness, generality, and an increased trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs at a scale and speed that were previously out of reach. In this paper, we evaluate the capabilities of LLMs to produce foundational, machine-checked proofs of refinement between executable code and its high-level specification, as post hoc, per-artifact certificates. We study this in the context of the Ethereum Virtual Machine (EVM), a low-level virtual machine that executes smart contracts on the Ethereum blockchain. We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a specification language that characterizes the intended behavior of smart contracts, but commits to no source language or compilation toolchain. In EquiVM, refinement is stated for deployed bytecode of arbitrary provenance, interaction with unknown code is part of the semantics, and each proof is a replayable, machine-checked certificate. No previous technique achieves this combination. Using frontier commercial LLMs, twenty-three real-world contracts are proved end to end with minimal human guidance, among them most of the MakerDAO stablecoin system, at up to a hundred million tokens and a hundred hours of proof time per contract. We conclude that foundational mechanized proofs can now be bought at the price of tokens, and that this shift can reshape how verification frameworks are architected.
