Verity

一个用 Lean 4 编写的形式化验证智能合约编译器，面向以太坊。
文档：veritylang.com  ·  论文：verity.pdf  ·  由 LFG Labs 构建

**Verity** 是一个用 [Lean 4](https://lean-lang.org/) 编写的形式化验证智能合约编译器。你可以在一个嵌入式 DSL 中编写合约，声明它们应该做什么，证明这些属性成立，并编译成 EVM 字节码。编译器本身被证明在三个验证层中都保持语义一致。完整文档位于 [**veritylang.com**](https://veritylang.com)。 | 指标 | 值 | |--------|-------| | 定理 | 283 (283 已证明, 0 sorry) | | 公理 | 0 | | Foundry 测试 | 522 (239 属性) | | 已验证合约 | 12 | | 核心 EDSL | 649 行 | | Lean | 4.22.0 | 以上每个数字都从代码库中提取，并在每次提交时进行验证。`0 sorry` 表示没有未完成的证明。`0 axioms` 表示编译器栈中没有未证明的假设。 ## 什么是经过验证的 Verity 证明编译在三个阶段保留了行为。每一层都是一个经过机器检查的 Lean 定理。 **第 1 层**（EDSL 到 CompilationModel）：`verity_contract` 宏从一个定义生成一个可执行的 Lean 程序和一个面向编译器的模型。每个合约的桥接定理证明它们是一致的。 **第 2 层**（CompilationModel 到 IR）：一个通用的全合约定理覆盖了支持的片段，且没有公理。不需要为每个合约单独证明。 **第 3 层**（IR 到 Yul）：所有语句类型都被证明是等价的。调度桥接是一个显式的定理假设，而不是公理。 Yul 到字节码的步骤由 `solc`（v0.8.33，已固定版本）处理，并且没有被 Verity 验证。完整的信任边界请参见 [TRUST_ASSUMPTIONS.md](TRUST_ASSUMPTIONS.md)。 ## 工作原理 ``` verity_contract Counter where storage count : Uint256 := slot 0 function increment () : Unit := do let current <- getStorage count setStorage count (add current 1) ``` ``` theorem increment_correct (s : ContractState) : let s' := ((increment).run s).snd s'.storage 0 = add (s.storage 0) 1 := by rfl ``` 证明通过 `rfl`（自反性）通过：Lean 的内核计算两边并确认它们在定义上相等。没有外部求解器，没有有界模型检查器，除了 Lean 的类型论之外不信任任何东西。 ## 快速开始 ``` curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh source ~/.elan/env git clone https://github.com/lfglabs-dev/verity.git && cd verity lake build # verify all proofs (~20 min first build) make check # run full CI validation suite FOUNDRY_PROFILE=difftest forge test # differential tests: EDSL vs EVM ``` ## Verity 的对比 | | Certora | Halmos | Verity | |---|---|---|---| | **方法** | 有界模型检查 | 符号执行 | 在 Lean 4 中进行定理证明 | | **证明范围** | 有界（可配置深度） | 有界（路径爆炸） | 无界（所有输入，所有路径） | | **编译器信任** | 完全信任 solc | 完全信任 solc | 验证 3 个编译层 | | **最适合** | 大规模生产审计 | 在 Foundry 中查找 bug | 高保障合约 | Verity 与这些工具是互补的。它适用于你需要跨越所有输入和所有执行路径的数学确定性的场景。 ## 文档 | 资源 | 描述 | |----------|-------------| | [veritylang.com](https://veritylang.com/) | 完整文档站点 | | [Solidity 到 Verity](https://veritylang.com/guides/solidity-to-verity) | 用于 Solidity 移植的实用语法和语义映射 | | [生产 Solidity 模式](https://veritylang.com/guides/production-solidity-patterns) | 生产移植的代理指南、可重用的 Verity 特性以及预言机/规范边界 | | [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md) | 定理计数、证明状态、测试覆盖率 | | [TRUST_ASSUMPTIONS.md](TRUST_ASSUMPTIONS.md) | 哪些是经过验证的，哪些是被信任的 | | [AXIOMS.md](AXIOMS.md) | 已记录的公理（当前为 0） | | [AUDIT.md](AUDIT.md) | 信任边界审计证据和 CI 防护 | | [CONTRIBUTING.md](CONTRIBUTING.md) | 贡献指南 | ### 研究 - [Verity: 一个形式化验证的智能合约编译器](https://lfglabs.dev/papers/verity.pdf) - [Verity 基准测试：AI 驱动的证明生成](https://lfglabs.dev/research/verity-benchmark) - [什么是形式化证明？](https://lfglabs.dev/research/what-is-a-formal-proof) ## 支持 Verity 是一项公益项目。如果你想支持该项目，可以通过 Giveth 捐款： [verity: AI 时代的智能合约安全](https://giveth.io/project/verity:-smart-contracts-security-for-the-age-of-ai)

标签：EVM, Lean 4, Web3, 以太坊, 区块链, 区块链安全, 去中心化应用, 去中心化金融, 安全性, 形式化方法, 形式化验证, 数学证明, 智能合约, 智能合约安全, 正确性, 编程语言, 编译器, 编译器设计, 软件验证, 领域特定语言