以太坊形式化验证相关项目汇总

liumuhui 3小时前阅读数 1 #区块链

文章标签形式化验证智能合约 EVM Solidity Vyper 以太坊

本页概述了以太坊生态中的形式化验证（及相关分析）项目。它是对 pirapira/ethereum-formal-verification-overview 的扩展和更新。

重点是智能合约的形式化验证和其他类型的分析，同时也收集了协议和编译器的形式化验证信息。

这些列表并不完整，建议访问项目页面以了解更多信息。

如果你有此处未包含的信息或发现错误，欢迎随时提交 issue/PR。

维护状态： 标记为 ️ 的项目已归档，或截至 2026 年 6 月已超过一年没有提交。它们被保留下来作为历史参考；不活跃的项目可能仍然完全可用。

智能合约

有多个项目致力于智能合约的形式化规范和验证。以下列表按目标语言/技术分类，并按字母顺序排列。每个项目都附有一些资源链接；如需了解更多，请访问项目页面。

此外，还有大量论文描述了与智能合约形式化验证相关的技术。例如，访问 ntu-srslab/smart-contract-publications 并在搜索框中输入 2020。因此，对于我找不到实际工具的论文，这里不再列出。

学习

Formal Methods for DeFi Developers：为培训开发者使用和开发形式化方法与工具而设计的系列课程。️ 自 2022-07 起没有提交。

规范

Act：Act 允许对存储更新、前置/后置条件和合约不变量进行规范描述。其工具套件还提供证明后端，可通过 Coq、SMT 求解器或 hevm 证明许多属性。
- 文章：Act 0.1 Release & Tutorial，David Terry。
- 演讲：Smart contracts as inductive systems，Martin Lundfall。
Certora Verification Language (CVL)：Certora Prover 使用它来为被分析的合约编写属性。
Scribble：Scribble 是一款面向 Solidity 的运行时验证工具，它将 Scribble 规范语言中的注解转换为具体断言，以检查规范。

模糊测试

Echidna：一个快速的智能合约模糊测试器。它专为模糊测试和基于属性的测试而设计。
Harvey：一个针对以太坊智能合约的模糊测试器。
hevm：如你将在下文看到的，hevm 用途广泛，其中就包括作为模糊测试器。该模糊测试器也可用于尝试打破不变量。
- 文章：Symbolic Execution With ds-test，David Terry。
ItyFuzz：基于快照的混合模糊测试器，针对 EVM（和 MoveVM）字节码，将模糊测试与符号执行相结合，以快速到达深层状态。
- 论文：ItyFuzz: Snapshot-Based Fuzzer for Smart Contract，Chaofan Shou、Shangyin Tan、Koushik Sen（ISSTA 2023）。

经济学 / 博弈论

Clockwork Finance Framework：一个通用的形式化验证框架和机械化证明系统，用于推理组合式 DeFi 合约的经济安全属性，使用 K 框架的符号执行引擎和模型检查器。️ 自 2021-09 起没有提交。
- 论文：Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts
- 演讲：Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts - SBC22
- 幻灯片：Clockwork Finance

EVM 字节码

Blanc：一种基于 Lean 4 的 EVM 编程语言，具有编译器正确性和 WETH 偿付能力证明。
Certora
- 论文：Finding Bugs Automatically in Smart Contracts with Parameterized Invariants，Thomas Bernardi 等人（2020）
EquiVM：Lean 4 中的精化证明，证明 EVM 字节码实现了用 Sol⁻（一种类似 Solidity 的规范语言）编写的高级程序；此类高级程序旨在由 LLM Agent 生成。
EthBMC：一个面向智能合约的有界模型检查器。️ 自 2022-12 起没有提交。
EtherTrust：一款 EVM 字节码分析工具。
- 论文：Foundations and Tools for the Static Analysis of Ethereum smart contracts，Ilya Grishchenko 等人（2018）。
EthIsabelle：EVM 的 Lem 形式化及一些 Isabelle/HOL 证明。️ 自 2022-03 起没有提交。
- 演讲：Formal Verification of Smart Contracts，Yoichi Hirai。
eThor：面向以太坊智能合约的静态分析工具。
EVM-Dafny：用 Dafny 编写的、形式化且可执行的 EVM 语义。
- 论文（FM23）：Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny，Franck Cassez 等人（2023）。
- 论文（arXiv 版本）：Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny，Franck Cassez 等人（2023）。
evm-sail：用 Sail 编写的、形式化且可执行的 EVM 规范，Sail 是官方 RISC-V 模型背后的 ISA 规范语言，可导出到 Coq、Isabelle/HOL、HOL4 和 Lean。
- 文档：evm-sail documentation and benchmarks。
EvmSemantics：Lean 4 中 EVM 的关系式小步和大步语义，并带有一个可执行解释器，该解释器已被证明相对该关系是健全的。
evm-smith：一个供 AI 系统编写 EVM 字节码并证明其安全的框架，基于 EVMYulLean 构建。
EVMYulLean：Lean 4 中 EVM 和 Yul IR 的可执行形式化模型。
GASOL：一个通用框架，通过应用一种被称为“超级优化”的技术来优化智能合约，该技术包括优化基本块。
- 论文：A Max-SMT Superoptimizer for EVM handling Memory and Storage。Elvira Albert、Pablo Gordillo、Alejandro Hernández-Cerezo 和 Albert Rubio，TACAS 2022。
- 论文：Super-Optimization of Smart Contracts。Elvira Albert、Pablo Gordillo、Alejandro Hernández-Cerezo、Albert Rubio 和 Maria A. Schett，2022。
Halmos：符号测试工具（a16z），通过符号执行 Foundry/Solidity 测试来证明或反驳针对所有可能输入的断言。
hevm：针对 EVM 代码的符号执行引擎和等价性检查器。
- 文章：Symbolic Execution With ds-test，David Terry。
- 文章：Symbolic execution for hevm，Martin Lundfall。
Jaune：Lean 4 中 EVM 的可执行形式化规范。
KEVM：以太坊虚拟机（EVM）的 K 语义。
- 演讲：KEVM Overview。
- 论文：KEVM: A Complete Semantics of the Ethereum Virtual Machine，Everett Hildenbrandt 等人（2017）。
Kontrol：结合 KEVM 和 Foundry，让开发者可以直接从其 Solidity 测试套件中运行 K 框架的符号执行证明。
Manticore：基于符号执行的 EVM 字节码分析工具。
- 文章：Manticore: Symbolic execution for humans。
- 研讨会：Using Manticore and Symbolic Execution to Find Smart Contracts Bugs - Devcon IV。
MAIAN：EVM 字节码分析工具，检查合约是否可能具有自杀性、挥霍性或贪婪性。️ 自 2023-10 起没有提交。
- 论文：Finding The Greedy, Prodigal, and Suicidal Contracts at Scale，Ivica Nikolic 等人（2018）。
Mythril：一款使用 concolic 分析、污点分析和控制流检查的 EVM 字节码安全分析工具。
- 文章：Practical Smart Contract Security Analysis and Exploitation— Part 1，Bernhard Mueller。
Securify：以太坊智能合约安全扫描器。️ 自 2025-05 起没有提交。
- 论文：Securify: Practical Security Analysis of Smart Contracts，Petar Tsankov 等人（2018）。
Verifereum：EVM 的规范，以及在 HOL4 中对 EVM 字节码的完整功能验证。
VerX：以太坊智能合约的完整功能验证。
- 论文：VerX: Safety Verification of Smart Contracts，Permenev 等人（2019）。
KLab：K 框架的证明浏览器及智能合约规范格式。️ 已归档；自 2021-08 起没有提交。
- 教程：KLab，Everett Hildenbrandt。
- 研讨会：Formal Verification Workshop Using KLab - Devcon IV。未能找到视频/幻灯片。
Oyente：基于符号执行的 EVM 字节码分析工具。️ 已归档；自 2023-01 起没有提交。
- 论文：Making Smart Contracts Smarter，Loi Luu 等人（2016）。

Solidity

Clear：面向 Yul/Solidity 程序的交互式形式化验证框架，基于 Nethermind 用 Lean 编写的 Yul EVM 方言模型。
Pyrometer：结合抽象解释、符号执行和静态分析，对 Solidity 进行值范围和可达性（界）分析。️ 自 2025-02 起没有提交。
Slither：用于检测特定漏洞的 Solidity 静态分析框架。
- 文章：Slither – a Solidity static analysis framework。
SmartAce：一个用于智能合约验证的自动化框架。️ 自 2022-01 起没有提交。
- 论文：Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE，Scott Wesley 等人（2022）。
SmartCheck：用于发现 Solidity 合约漏洞的静态分析工具。️ 自 2023-05 起没有提交。
- 论文：SmartCheck: static analysis of ethereum smart contracts，Sergei Tikhomirov 等人（2018）。
Solidifier：Solidity 的有界模型检查器。️ 自 2020-12 起没有提交。
- 论文：Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling，Pedro Antonino 和 A. W. Roscoe（2021）。
Solidity 的 SMTChecker：一个内置于 Solidity 编译器中的、基于 SMT 和 Horn 的模型检查器，在编译时静态检查安全属性，并考虑无限数量的交易。
- 幻灯片：Formally Verifying Ethereum Smart Contracts by Overwhelming Horn Solvers，Dagstuhl 智能合约严谨方法研讨会，Leonardo Alt。
- 演讲：Fully Automated Formal Verification: How far can we go? - EthCC 4，Leonardo Alt 和 Martin Lundfall。
- 幻灯片：Fully Automated Formal Verification: How far can we go? - EthCC 4，Leonardo Alt 和 Martin Lundfall。
- 文章：Automated Synthesis of External Unknown Functions，Leonardo Alt。
- 演讲：Fully Automated Inductive Invariants Inference for Solidity Smart Contracts - Devcon V，Leonardo Alt。
- 幻灯片：Fully Automated Inductive Invariants Inference for Solidity Smart Contracts - Devcon V，Leonardo Alt。
- 文章：SMTChecker Toward Completeness，Leonardo Alt。
- 论文：Accurate Smart Contract Verification through Direct Modelling，Matteo Marescotti、Rodrigo Otoni、Leonardo Alt、Patrick Eugster、Antti E. J. Hyvärinen 和 Natasha Sharygina（2020）。
- 论文：SMT-Based Verification of Solidity Smart Contracts，Leonardo Alt 和 Christian Reitwiessner（2018）。
solc-verify：通过注解和模块化程序验证，对 Solidity 代码进行功能验证。️ 自 2023-09 起没有提交。
- 论文：solc-verify: A Modular Verifier for Solidity Smart Contracts，Á. Hajdu、D. Jovanović（2019）。
- 演讲：solc-verify, a source-level formal verification tool for Solidity smart contracts，由 Á. Hajdu 在 Solidity Summit（2020）上讲授。
- 论文：SMT-Friendly Formalization of the Solidity Memory Model，Á. Hajdu、D. Jovanović（2020）。
- 演讲：SMT-Friendly Formalization of the Solidity Memory Model，由 Á. Hajdu 在 SMT（2020）上讲授。
- 论文：Formal Specification and Verification of Solidity Contracts with Events，Á. Hajdu、D. Jovanović、G. Ciocarlie（2020）。
- 演讲：Formal Specification and Verification of Solidity Contracts with Events，由 Á. Hajdu 在 FMBC（2020）上讲授。
VeriSmart：Solidity 智能合约的安全验证器，基于合约不变量的自动推断。️ 自 2023-01 起没有提交。
VeriSol：使用代码合约、Boogie 和 Corral 对 Solidity 智能合约进行形式化规范、验证和可扩展的反驳。️ 自 2022-12 起没有提交。
- 幻灯片：Formal Verification of Smart Contracts and Protocols: What, Why, How - Devcon V，Shuvendu Lahiri 等人。
- 文章：Researchers work to secure Azure Blockchain smart contracts with formal verification，微软研究院博客。
- 论文：Formal Specification and Verification of Smart Contracts for Azure Blockchain，Yuepeng Wang、Shuvendu K. Lahiri、Shuo Chen、Rong Pan、Isil Dillig、Cody Born、Immad Naseer。
Verity：一个基于 Lean 的 EDSL，用于对以太坊智能合约进行规范、实现和证明，并将经过验证的合约编译为 EVM 字节码，附有机器检查的规范/实现等价性。（veritylang.com）
Wake：一个 Python 框架，集成了 Solidity 静态分析检测器框架、基于属性的模糊测试和开发者工具。

Vyper

Vyper-HOL：Vyper 的语义，以及在 HOL4 中对 Vyper 的已验证编译。
2vyper：基于 Viper 验证基础设施的 Vyper 智能合约自动验证器。️ 自 2023-02 起没有提交。
FVyper：使用形式化方法（KEVM）开发的一组实用 Vyper 合约。️ 已归档；自 2021-04 起没有提交。
KVyper：Vyper 在 K 中的语义。️ 自 2018-08 起没有提交。

编译器与中间语言

Solidity / Yul

Yul-ACL2。在 ACL2 框架中形式化的 IR Yul 语义。
yul-compiler：Lean 4 中一个经过验证的编译器，将 Yul 的一个片段编译为 EVM 字节码。它已证明相对于 yul-semantics 和 EvmSemantics 是正确的；对于无法验证的内容，它会予以拒绝，而不是生成未经验证的代码。
Yul-Isabelle。在 Isabelle 中形式化的 IR Yul 语义。️ 自 2022-11 起没有提交。
Yul-Lean：Lean 证明助手中 Yul IR 语义的形式化规范。
- 文章：Securing Warp: A formal specification of the Yul IR，Julian Sutherland。
yul-semantics：Lean 4 中 Yul 的无 Gas 大步关系语义，以抽象方言为参数，并带有一个已被证明充分的可执行解释器。
Solidity Optimizer Transformations。在 ACL2 中形式化，并验证 Solidity 编译器中的一些 Yul 优化器变换的正确性。
Yul-K：在 K 框架中形式化的 IR Yul 语义。️ 已归档；自 2019-10 起没有提交。

以太坊协议

共识层

此前被称为“Eth2”/“Ethereum 2.0”（即信标链及其“Phase 0”部署）。此后，Eth1/Eth2 术语已被弃用，转而使用“执行层”和“共识层”。

SizzLean：SSZ 的 Lean 4 实现。SSZ 是以太坊共识层的序列化和 Merkle 化格式。该实现针对固定大小类型证明了往返、不可延展性和大小界定理，并完全符合上游 consensus-spec-tests。
存款合约（Runtime Verification）：对 Eth2 存款合约的端到端形式化验证。
- 第 1 部分
- 第 2 部分
Formal Verification of the Eth2.0 Specs in Dafny：在具备验证能力的编程语言 Dafny 中，为 Eth2.0 规范建立形式化规范。️ 已归档；自 2024-06 起没有提交。
- 论文：Formal Verification of the Ethereum 2.0 Beacon Chain，Franck Cassez、Joanne Fuller、Aditya Asgaonkar。
Fully Mechanised Proof of the Deposit Contract's Incremental Merkle tree algorithm in Dafny。️ 已归档；自 2021-09 起没有提交。

零知识应用与算术电路

Semaphore 的 ACL2 形式化
- Semaphore
- ACL2 Semaphore Docs
使用 Lean 进行 Cairo 验证
- 论文：A verified algebraic representation of Cairo program execution，Jeremy Avigad 等人。
circomspect：Trail of Bits 的 Circom 电路静态分析器/linter，包含多个分析遍次，可标记约束不足的信号及其他电路错误。️ 自 2024-06 起没有提交。
circuzz：针对零知识电路编译器工具链的蜕变和差分模糊测试流水线。
CIVER：Circom 电路的模块化验证器，用于验证弱安全性（不存在约束不足的信号）、标签规范以及前置/后置条件。
Coda：一种用于 ZK 电路的静态类型语言，具有精化类型系统，可将证明义务交由 Coq 处理。
Ecne：一个用于验证 R1CS 约束健全性的引擎。️ 自 2022-08 起没有提交。
gnark-lean-extractor：将在 Go 中定义的 gnark（zk-SNARK 库）电路提取到 Lean 中进行形式化验证。️ 自 2025-04 起没有提交。
Korrekt (halo2-analyzer)：使用抽象解释和 SMT 来检测 Halo2（PLONKish）电路中的约束不足单元及未使用的门/列。
Leo
- 论文：LEO: A Programming Language for Formally Verified, Zero-Knowledge Applications
Picus：用于 ZKP 电路（Circom、R1CS、gnark）唯一性/约束不足属性的自动化验证器（Veridise），使用 SMT 求解器。️ 自 2024-03 起没有提交（一个积极维护的分支位于 chyanju/Picus）。
Verified zk(E)VM：一项研究计划，旨在加速将形式化验证应用于 Lean 中的 zk(E)VM（verified-zkevm.org）。
- ArkLib：Lean 中经过形式化验证的知识论证。
- clean：一个经过验证的 Lean 电路 DSL。
- evm-asm：Lean 4 中一个实验性的经过验证的宏汇编器，基于 RISC-V RV64IM 后端，目标是构建一个可信计算基中不包含编译器的 zkEVM 无状态区块验证器。
zkFuzz：针对 ZK 电路的程序变异模糊测试框架，将轨迹-约束一致性测试形式化，以发现约束不足/约束过度错误。