paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A formal verification tool for Ethereum VM bytecode

面向以太坊虚拟机字节码的形式化验证工具
FSE Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2018匹配度 3/10 · 论文属于形式化验证与定理证明工具，与用户对形式化验证的兴趣有较弱交集，但未涉及 LLM/Agent 改进验证、浮点程序分析或贝叶斯程序分析，也不在 PL→AI 或 AI→PL 的核心主线上。引用 109 inbox
Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, Grigore Roşu
程序验证定理证明与证明工程
crossref: 2026-09-12

AI 速览

一句话：基于KEVM形式语义与K框架可达性逻辑，构建并优化了EVM字节码演绎验证器，成功验证多个知名智能合约。

本文提出一个针对以太坊虚拟机（EVM）字节码的形式化验证工具。为精确推理EVM字节码的所有可能行为，作者采用KEVM——EVM的完整形式语义，并实例化K框架的可达性逻辑定理证明器，从而得到一个构造正确的EVM演绎验证器。为提升可扩展性，作者进一步引入EVM专用的抽象与引理对验证器进行优化。该验证器已被用于验证多个高知名度智能合约，包括ERC20代币、以太坊Casper以及DappHub MakerDAO合约，表明其具备处理真实复杂合约的能力，为EVM字节码的形式化验证提供了实用且可扩展的途径。

问题
EVM字节码行为复杂，缺乏能够精确推理其所有可能行为的形式化验证工具。
方法
采用KEVM完整形式语义，实例化K框架的可达性逻辑定理证明器以生成构造正确的演绎验证器，并引入EVM专用抽象与引理优化可扩展性。
评估
将验证器应用于ERC20代币、以太坊Casper和DappHub MakerDAO等知名智能合约，验证其有效性与可扩展性。
原文摘要（Abstract）

In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4585,
  title = {A formal verification tool for Ethereum VM bytecode},
  author = {Daejun Park and Yi Zhang and Manasvi Saxena and Philip Daian and Grigore Roşu},
  booktitle = {FSE},
  year = {2018},
  doi = {10.1145/3236024.3264591}
}