作者：@dvzhangtz；来源：作者推特@dvzhangtz
最近看了一些形式化验证的项目，感觉在新周期中其依旧会是有趣的叙事。
但该技术作为合约安全中最重要的组成，却在推上几乎看不到中文帖。所以总结了一下学习中得到的认知...
现在，你可以用五分钟拿走这些认知。
背景：智能合约是区块链世界核心之一，合约发生安全问题，Dapp 中的钱就全部凉凉。 根据 Rekt 榜上可以看到，因为合约安全造成的直接损失单次最高达 $ 600M，间接损失更加严重，合约不安全会令社区对项目失去信心。 https://rekt.news/leaderboard/
传统上如果为了让合约更安全，思路是叠甲，比如：
1 使用标准函数包如 @OpenZeppelin 的包来写代码，让代码更安全
2 写完后使用一些工具进行初步筛查，看有没有问题
3 写一些测试程序，对合约分模块用样本数据测试
4 ......
但铠甲再厚也总会有漏洞，测试程序也只能用一些样本进行测试，不可能穷尽所有可能性。所以这些方法都只能降低出现安全问题的可能性，不能保证合约没有问题 有没有一种办法能像预言家验狼人一样，能确保合约没有某方面安全漏洞？ 答案是——形式化验证
想进行一次形式化验证，需要几步：
1. 写形式化规范，里面定义我们想要验证的东西
2. 使用形式化分析框架验证，这类工具会自动验证合约是否符合我们定义的规范
3. 发现某些情况下出现问题
4. 改代码解决问题
一个真实案例：巫师决斗 @CHZWZRDS
https://github.com/dapperlabs/cheezyverse/blob/fef271db4c18c00949de291da0b46a1397216306/contracts/BasicTournament.sol#L2059…
下面的代码时说：在游戏超时时，巫师 1 会吸走巫师 2 的能量，巫师 2 能量清零。
作为一个 gamefi，这个能量自然很重要。
理论上这个能量只能在两个巫师之间转移，但如果黑客发现这段程序的漏洞，可以让能量凭空增加 / 消失，无疑会对这个 Gamefi 造成重大影响。
使用正常的安全验证方式，我们用了几个测试数据，发现一切都运行的很 nice，我们甚至准备直接上链部署了。 不过等等，为什么不试试形式化验证？
第一步：定义形式化规范
我们希望能量只会在巫师之间相互转移，不会凭空增加/消失，也就是： wiz1.power + wiz2.power = old_wiz1.power + old_wiz2.power 。
第二步：形式化分析框架自动验证
这类工具实质上是一种用于探索合约执行的所有可能路径的技术，以确保在所有可能的执行路径上都满足规范。
第三步：发现问题
发现了一个问题！一个神奇的问题，如果决斗的两个巫师是一个人，也就是决斗双方的地址一致，就会让该用户的能量清零！ 第四步：改正问题 既然发现了问题，其实很容易改，我们只需要加一行代码，预先审核，确保决斗双方不是一个人就好啦～
类似的问题还有经典的 K 值校验问题。Uniswap 的核心是恒定乘积模型 K=x*y，其中的 K 值是该 pair 合约持有代币数量的乘积，且要求之后的每一笔交易完成后 K 值须增加(手续费) 如果有黑客发现了合约中的漏洞，可以使得自己的交易不用符合恒定乘积，这样合约就是提款机了，用上文思路也可避免该问题。
从上文可以感受到形式化验证的几个特点：
1. 终局性：在所验证问题上可以证出合约不存在某些问题；
2. 对规范的依赖(严重)：上文只是验证了一个规范，但实际合约会面临的问题很多，我们可能会漏掉某些规范，而书写规范本身也是比较耗人力的，所以形式化验证主要是对合约一些关键属性进行验证。
3. 性能问题(严重)：使用形式化分析框架自动验证，本质上是探索合约执行的所有可能路径上都符合规范，这有可能会遇到状态爆炸和路径爆炸问题，同时其底层使用 SMT 求解器和其他约束求解器，这些求解器也是耗算力的大户。 所以，未来将这件事以一个什么样的方式外包出去降低成本，也许能促进其发展。
如果想进行形式化验证，相关工具如下：
书写形式化规范的语言
Act: https://github.com/ethereum/act
Scribble: https://docs.scribble.codes
Dafny: https://github.com/dafny-lang/dafny…
用于检验正确性的验证器
Certora Prover: https://docs.certora.com/en/latest/index.html…
Solidity SMTChecker: https://github.com/ethereum/solidity…
solc-verify: https://github.com/SRI-CSL/solidity…
