登链社区

确保以太坊安全：ZK-EVM形式化验证项目

视频 AI 总结：本视频中，Veridise的CEO Kostas Fernandes与以太坊基金会Alexander Higgs讨论了ZKVM验证计划。核心目标是确保ZKVMs（零知识虚拟机）的安全性，以支持以太坊L1的扩展。项目分为三个轨道：ZKVM电路、EVM访客程序和密码学证明系统，已取得显著进展，包括RISC-V电路的形式化验证和证明速度优化。最终目标是在2026年实现L1上的可选证明，并逐步过渡到强制证明，以提升性能和安全性，同时引入LLZK等工具链推动编译和验证的标准化。关键信息： - ZKVM对以太坊扩展至关重要，可替代重执行，提高gas限值。 - 项目分三轨：验证ZKVM电路安全性、EVM访客程序的正确性、以及证明系统的形式化规范。 - 主要进展：RISC-V电路已针对SAIL规范完成形式化验证；证明时间从数月缩短至10周；预编译（如Keccak）验证取得成果。 - LLZK（基于MLIR的中间表示）用于统一电路编译，支持多DSL并集成验证后端。 - 目标时间线：2026年实现L1可选证明，2027-2028年实现强制证明。 - 未来影响：ZKVMs将改变执行层和共识层，可能推动EVM演变或直接支持RISC-V智能合约，编译器工具链成为关键。 Timestamps: 00:00 Introductions 00:16 What are the main goals of the Ethereum Foundation’s ZK-EVM Verification Project? 02:12 Current progress: what has been accomplished so far, and what’s coming next? 20:57 Deep dive into LLZK: Current use cases. What developers are building now and in the future? 32:47 Where to learn more about the mentioned LLZK projects and how to contribute? 34:20 The future of Ethereum, the EVM, and ZK-VMs: will users interact with ZK-VMs or L1 directly? 40:00 Could ZK-VMs eventually replace the EVM? 45:33 Closing remarks

241 0 0 2026-05-29 08:30

以太坊执行层精简路线图 2026 至 2030

视频 AI 总结：本视频围绕以太坊“Lean Execution”路线图展开，重点讨论通过 ZKVM、形式化验证和协议改进，逐步把以太坊推向更高吞吐、低成本且保持去中心化的“终局”。演讲者介绍了从可选证明、强制证明到规范化实现的演进路径，并说明数据层、状态管理、抗审查机制与 RISC-V/Lean4 等技术如何协同支撑未来升级。关键信息： 1. 以太坊长期目标是实现约 1 Giga gas/s 的 L1 吞吐，并扩展到全 L2 约 10M TPS。 2. ZKVM 通过“验证证明”替代“重新执行区块”，同时提升扩容与去中心化。 3. 证明将经历三阶段：可选证明、强制证明、最终规范化证明/规范化实现。 4. 证明延迟、证明大小、带宽开销是核心挑战，需依赖延迟执行、分片广播等优化。 5. 证明者硬件目标是：成本低于 10 万美元、功耗低于 10 千瓦，以支持“家庭证明者”。 6. 需在 ZKVM 和 Guest 程序两层保持多样性，未来可能转向经形式化验证的单一规范实现。 7. Fossil、inclusion lists、validity-only partial state 等机制用于提升抗审查与状态可维护性。 8. 状态增长将通过多维收费、状态裁剪、状态过期等方式治理。 9. RISC-V 被视为重要的 ZK ISA 候选，未来可能成为 EVM 底层规范或直接暴露给开发者。 10. 形式化验证与 AI 工具被看好，可显著降低 ZKVM、证明系统和数学定理中的错误风险。

154 0 0 2026-04-16 09:48

DeFi 安全 101 - 从模糊测试到形式化验证

视频 AI 总结：该视频主要讲解了如何从模糊测试（Fuzzing）过渡到形式化验证（Formal Verification），并对比了两者的异同。核心观点是，模糊测试和形式化验证都是发现智能合约漏洞的工具，但形式化验证能提供更强的保证。视频通过一个计算二进制数中“1”的个数（pop count）的例子，以及一个简单的 Vault 合约的例子，演示了如何使用 Certora 的工具进行形式化验证，并强调了在智能合约开发中尽早同时使用这两种方法的重要性。视频中提出的关键信息： * **模糊测试 (Fuzzing)**：通过生成大量随机输入来测试代码，寻找违反预设属性的情况。虽然易于上手，但覆盖范围有限，只能提供概率性的保证。 * **形式化验证 (Formal Verification)**：通过数学证明来验证代码是否完全符合规范。可以覆盖所有可能的输入，提供更强的保证，但学习曲线较陡峭。 * **不变性 (Invariants)**：在合约的所有状态下都必须保持为真的属性。形式化验证可以用来证明不变性在合约的任何状态下都成立。 * **Certora Prover**：Certora 的形式化验证工具，可以将代码和规范编译成逻辑公式，并使用求解器来验证公式的有效性。 * **CVL (Certora Verification Language)**：Certora 的验证语言，用于编写形式化规范。 * **Solvency**：一种重要的 Vault 合约属性，指总的 shares 数量小于等于总的 tokens 数量。 * **尽早使用**：建议在智能合约开发的早期阶段就开始使用模糊测试和形式化验证，以便尽早发现并修复漏洞。

1685 0 0 2025-12-14 19:17

汇编与 EVM 课程 - Gas 2

视频 AI 总结：该视频主要讲解了如何使用 Certora 工具对智能合约进行形式化验证，特别是针对 Gas 优化后的合约进行等价性验证。视频通过一个 NFT 市场的例子，展示了如何定义 ghost 变量、使用 hooks 监控合约状态变化、编写 invariants 来验证合约行为，以及如何利用 method summaries 和 prover arguments 来解决验证过程中遇到的问题，最终实现对 Gas 优化合约的功能等价性证明。视频中提出的关键信息包括： 1. **Ghost 变量：** 用于在形式化验证中追踪合约状态，但不会影响合约的实际执行。 2. **Hooks：** 用于在特定 EVM 操作码执行时触发自定义逻辑，例如更新 ghost 变量。 3. **Invariants：** 用于声明合约状态必须满足的条件，Certora 会尝试找到违反这些条件的执行路径。 4. **Method Summaries：** 用于简化或替换合约中的函数行为，例如使用 `dispatcher` 关键字来限制外部调用的影响。 5. **Prover Arguments：** 用于配置 Certora 的行为，例如使用 `optimistic fallback` 来假设外部调用不会对合约状态产生任意修改。 6. **Parametric Rules：** 允许验证具有未定义方法变量的规则，用于比较不同合约在相同输入下的行为。 7. **Vacuity Checks：** 用于检测规则是否过于严格，以至于没有输入可以满足所有前提条件。 8. **等价性验证：** 通过比较 Gas 优化前后合约的 getter 函数返回值，证明它们在功能上是等价的。

1377 0 0 2025-10-08 16:22

汇编与 EVM 课程 - NFT 市场 gas 优化

**视频 AI 总结：** 该视频是 Assembly EVM Op Codes 和 Formal Verification 课程的最后一部分，旨在帮助学习者掌握汇编和形式化验证技术。视频的核心内容是演示如何使用形式化验证工具 Certora 来验证一个用 Solidity 编写的 NFT 市场合约和一个用汇编重写的、更节省 Gas 的版本是否等价。通过这个过程，学习者可以学习到如何确保汇编代码在功能上与 Solidity 参考实现一致，从而构建更高效的智能合约。 **视频中提出的关键信息：** * **CodeHawks 平台：** 学习者可以在完成课程后参与 codehawks 上的形式化验证竞赛，并有机会获得报酬。 * **Gas Bad NFT Marketplace 项目：** 该项目包含一个用 Solidity 编写的 NFT 市场合约（`nft_marketplace.sol`）和一个用汇编重写的版本（`gas_bad_nft_marketplace.sol`），汇编版本旨在节省 Gas 费用。 * **形式化验证目标：** 视频将演示如何使用 Certora 验证以下两点： * 每当映射（mapping）被更新时，都会发出一个事件（event）。 * Gas Bad NFT Marketplace 和 NFT Marketplace 在调用任何函数后，最终状态是相同的（除了 Gas 消耗的差异）。 * **Certora 的使用：** 视频将从头开始编写 Certora 的配置文件和规范文件，并介绍以下概念： * **Ghost 变量：** 用于在验证过程中定义额外的变量，以便在规则和Hook之间传递信息。 * **Hooks（Hook）：** 用于在特定的底层操作（如存储变量的加载和存储）上附加 CVL 代码。 * **Init State 和 Axiom：** 用于初始化 Ghost 变量，并确保初始状态始终为真。 * **参数化规则：** 包含未定义方法变量的规则，允许对多个方法进行验证。 * **NFT Mock 合约：** 视频首先使用一个简单的 NFT Mock 合约进行热身，验证总供应量（total supply）永远不会为负，以及铸造（mint）函数总是铸造一个 NFT。 * **乐观循环（Optimistic Loop）：** 在某些情况下，需要启用乐观循环来避免循环展开问题。 * **代码仓库：** 视频提供了与课程相关的 GitHub 代码仓库[链接](https://github.com/Cyfrin/assembly-evm-opcodes-and-formal-verification-course)，学习者可以在其中找到项目代码和资源。

1286 0 0 2025-10-06 20:24

汇编与 EVM 课程 - 形式化验证与 Halmos 和 Certora 工具

视频 AI 总结：该视频是关于使用形式化验证和符号执行来审计智能合约，特别是针对一个名为 "Math Master" 的代码库。该代码库包含用于定点数运算的算术库，包括 `molwod`、`molwodUp` 和 `sqrt` 函数，这些函数都大量使用了汇编代码。视频强调了形式化验证在发现模糊测试无法找到的 bug 方面的作用，并介绍了 Halmos 和 Certora 等工具。关键信息： * **核心内容：** 介绍使用形式化验证工具 Halmos 和 Certora 审计 Math Master 代码库，寻找汇编代码中的 bug。 * **关键信息：** * Math Master 代码库包含 `molwod`、`molwodUp` 和 `sqrt` 三个函数，用于定点数运算。 * 形式化验证可以发现模糊测试无法找到的 bug。 * 介绍了 Halmos 和 Certora 两种形式化验证工具。 * 强调了理解代码库属性和编写正确断言的重要性。 * 演示了如何使用 Halmos 和 Certora 查找 Math Master 代码库中的 bug，包括版本问题、内存指针覆盖和函数选择器错误。 * 讨论了形式化验证的局限性，例如路径爆炸问题。 * 介绍了模块化验证的概念，将复杂问题分解为更简单的子问题。 * 强调了代码审计中手动审查和工具辅助相结合的重要性。

1230 0 0 2025-10-06 11:17

汇编与形式化验证 EVM #1 课程介绍

视频 AI 总结：本视频是关于 EVM 汇编操作码和形式化验证智能合约的课程介绍，旨在帮助开发者和安全研究人员达到区块链知识的顶尖水平。课程内容包括反汇编智能合约、学习字节码、优化合约 Gas 消耗、使用 Yul 和 Huff 编写智能合约，以及形式化验证。通过三个项目实践，深入学习 Halmos 和 Certora 等工具，掌握形式化验证和 Fuzzing 的使用场景，提升智能合约开发和安全能力。关键信息： * 课程目标：成为区块链知识顶尖的开发者和安全研究人员。 * 课程内容： * 智能合约反汇编和字节码学习。 * 使用 Yul 和 Huff 编写 Gas 优化合约。 * 形式化验证工具 Halmos 和 Certora 的使用。 * Fuzzing 和形式化验证的结合应用。 * 目标学员：已经熟悉 Solidity 或 Vyper 的开发者，希望提升到更高水平。 * 课程特点：深入、高级、项目驱动，强调实践和工具使用。 * Vyper 和 Solidity 的比较：Vyper 和 Solidity 都是高级语言，可以保护开发者免于出错，例如 calldata 大小和意外发送 E 以及安全数学。而且它们都是很棒的语言。所以选择任何一个并享受乐趣。Huff 和 Yul 是很棒的语言，如果你需要非常具体的性能代码，或者你希望了解更多关于 EVM 的信息。我不建议将这些语言用于所有生产代码。但我认为它们对于学习和理解来说非常棒。

1680 0 0 2025-10-02 21:11

Jolt 开发路线图更新

视频 AI 总结：该视频介绍了 Jolt 项目在过去六个月的进展和未来计划。Jolt 是一种 RISC-V ZKVM，旨在提供快速的零知识证明。视频重点介绍了 Jolt 在支持 Rust 标准库和 RISC-V M 扩展后，主要解决了验证成本高和证明者空间使用大的问题。通过改进多项式承诺方案和批量处理，Jolt 的证明大小已从兆字节级别降至 200KB 以下，并有望进一步降低。未来，Jolt 将致力于通过折叠方案降低证明者空间使用，并探索基于哈希的承诺方案以进一步提高速度。此外，团队还将投入大量精力进行形式化验证，以确保 Jolt 实现的正确性。关键信息： * Jolt 在过去六个月主要解决了验证成本高和证明者空间使用大的问题。 * 通过改进多项式承诺方案和批量处理，Jolt 的证明大小显著降低。 * 未来计划包括通过折叠方案降低证明者空间使用，探索基于哈希的承诺方案以提高速度，以及进行形式化验证。 * Jolt 旨在成为在资源受限环境中进行证明的理想 ZKVM，同时保持领先的证明速度。 * 将会有两个版本的Jolt，一个使用椭圆曲线，另一个使用哈希。

1222 0 0 2025-07-08 17:18

高级 Web3 安全课程 | 第九部分

视频 AI 总结：该视频主要讲解了智能合约的形式化验证，强调其作为最高级别的测试手段，能够彻底证明合约在任何情况下的行为符合预期。与单元测试或模糊测试不同，形式化验证通过布尔公式将智能合约代码转换为 SMT 求解器可解释的形式，从而验证特定不变性。视频还介绍了如何使用 Solidity 内置的 SMT 检查器进行形式化验证，并通过实例演示了如何通过添加 require 语句来限制输入范围，从而使断言通过验证。关键信息： * 形式化验证基于布尔公式，通过 SMT 求解器检查公式的满足性。 * SMT 检查器通过检查布尔公式的否定的不可满足性来验证断言。 * 可以通过 require 语句限制输入范围，使断言通过形式化验证。 * SMT 检查器不仅可以用于断言验证，还可以用于检查溢出、下溢、除零等潜在问题。 * SMT 检查器有其局限性，对于过于复杂的代码可能无法证明。 * 视频还介绍了如何通过提供价值和建立联系来获取审计机会，以及如何通过参加竞赛来展示自己的能力。

1921 0 0 2025-07-03 15:24