课程介绍

帮助开发者从“测试代码”升级为“数学证明代码正确性”，进入高安全等级的 Web3 工程与审计领域。

本课程由 RareSkills 提供，系统讲解如何使用 Certora Prover 和 CVL（Certora Verification Language） 对 Solidity 智能合约进行形式化验证。课程目标是帮助开发者从“测试代码”升级为“数学证明代码正确性”，进入高安全等级的 Web3 工程与审计领域。

一、内容概览

围绕真实工程场景展开，主要包括：

1）CVL 规则与基础语法

  • Formal Verification 基本原理
  • require / assert / satisfy 的形式化表达
  • 参数化规则（Parametric Rules）
  • 方法属性验证
  • 实际案例：验证 OpenZeppelin 的 Ownable、Initializable 等模块

这一部分的目标是：学会把“安全假设”写成数学规则。

2）高级验证能力（工程级）

  • Invariant（系统不变量）设计
  • Storage Hooks 与 Ghost Variables
  • 状态约束与路径爆炸处理
  • 循环验证策略
  • 实战验证：
    • ERC-20
    • WETH
    • ERC-721（Mint / Transfer / Approval 等）

重点能力：对完整协议级状态安全进行证明，而不仅是单函数测试。

二、适合人群

1）中级及以上 Solidity 开发者（强烈推荐）

  • 已有项目开发经验
  • 熟悉 ERC20 / ERC721 等标准
  • 想提升安全能力或进入高端岗位

你需要具备中等水平的 Solidity 基础，并熟悉常见 ERC 标准。

2）智能合约审计工程师 / 安全研究员 如果你的目标是：

  • 进入顶级审计公司
  • 提供高端安全服务
  • 做协议级安全保证

Certora 是目前头部审计机构的核心工具之一 。

3）DeFi / 协议开发负责人 特别适合：

  • 管理 TVL 较大的协议
  • 希望在上线前进行严格安全证明
  • 想建立工程级安全流程

4）希望进入高薪 Web3 安全赛道的人 当前 Web3 技术能力梯度：

能力层级 市场定位
单元测试 普通开发
Fuzz / Foundry 中级
形式化验证 顶级工程 / 审计

这门课程属于高阶护城河能力。