智能合约形式化验证方法 · 课程目录

01 形式化验证概述

什么是形式化验证
为什么需要形式化验证
在智能合约安全中的地位

进入章节 →

02 数学基础

命题逻辑
谓词逻辑
集合论基础
归纳法原理

进入章节 →

03 模型检测入门

状态空间
迁移系统
时态逻辑 LTL/CTL
模型检测算法概述

进入章节 →

04 符号执行

符号执行原理
路径约束
符号执行引擎
Manticore / hevm

进入章节 →

05 抽象解释

抽象域
伽罗瓦连接
不动点理论
在智能合约分析中的应用

进入章节 →

06 定理证明

Coq/Isabelle基础
归纳证明
函数式编程与证明
在合约验证中的实践

进入章节 →

07 SMT求解器

SAT/SMT问题
Z3基础
位向量与数组理论
在合约分析中的应用

进入章节 →

08 智能合约漏洞模型

重入攻击
整数溢出
访问控制
闪电贷攻击的形式化建模

进入章节 →

09 Solidity到中间表示

Solidity AST
Yul/IR
EVM字节码
控制流图构建

进入章节 →

10 EVM形式化语义

黄皮书解读
EVM操作码语义
Gas模型
存储模型

进入章节 →

11 不变式与断言

合约不变式
循环不变式
断言检查
Dafny语言简介

进入章节 →

12 静态分析工具

Slither
Mythril
Securify原理与对比
实际使用案例

进入章节 →

13 动态分析工具

Echidna
Diligence Fuzzing
Foundry fuzz测试
覆盖率引导

进入章节 →

14 形式化验证工具链

Certora Prover
VerX
KEVM
Halmos

进入章节 →

15 Certora Prover实战

规则编写
CVL语言
场景配置
实际合约验证案例

进入章节 →

16 KEVM与K框架

K框架基础
KEVM语义定义
合约形式化验证

进入章节 →

17 Coq验证实战

在Coq中建模EVM
证明合约属性
实际案例

进入章节 →

18 Isabelle/HOL验证实战

高阶逻辑
合约建模
自动化证明策略

进入章节 →

19 重入攻击的形式化验证

建模重入
验证防护措施
工具实践

进入章节 →

20 访问控制漏洞验证

角色模型
权限验证
时间锁的形式化分析

进入章节 →

21 DeFi协议验证

AMM模型
借贷协议
闪电贷的形式化建模

进入章节 →

22 NFT合约验证

ERC721标准
元数据
市场合约的形式化验证

进入章节 →

23 治理合约验证

DAO投票
提案执行
治理攻击的形式化分析

进入章节 →

24 跨链桥验证

跨链消息传递
验证器集合
资金安全的形式化建模

进入章节 →

25 Gas优化与形式化

Gas消耗建模
优化验证
循环Gas分析

进入章节 →

26 组合性验证

合约组合
接口契约
模块化验证方法

进入章节 →

27 升级合约验证

代理模式
存储布局
升级安全性形式化分析

进入章节 →

28 形式化验证与审计流程

审计中的形式化方法
报告编写
工具集成

进入章节 →

29 前沿研究

零知识证明验证
形式化验证与AI结合
新范式

进入章节 →

30 综合实战项目

完整DeFi协议的形式化验证
从需求到报告的全流程

进入章节 →