最近看了一些形式化验证的项目，感觉在新周期中其依旧会是有趣的叙事。但该技术作为合约安全中最重要的组成，却在推上几乎看不到中文帖。所以总结了一下学习中得到的认知...现在，你可以用五分钟拿走这些认知。背景：智能合约是区块链世界核心之一，合约发生安全问题，Dapp中的钱就全部凉凉。
根据Rekt榜上可以看到，因为合约安全造成的直接损失单次最高达$600M，间接损失更加严重，合约不安全会令社区对项目失去信心。https://rekt.news/leaderboard/传统上如果为了让合约更安全，思路是叠甲，比如：1使用标准函数包如@OpenZeppelin的包来写代码，让代码更安全2写完后使用一些工具进行初步筛查，看有没有问题3写一些测试程序，对合约分模块用样本数据测试4......但铠甲再厚也总会有漏洞，测试程序也只能用一些样本进行测试，不可能穷尽所有可能性。所以这些方法都只能降低出现安全问题的可能性，不能保证合约没有问题有没有一种办法能像预言家验狼人一样，能确保合约没有某方面安全漏洞？答案是——形式化验证想进行一次形式化验证，需要几步：1.写形式化规范，里面定义我们想要验证的东西2.使用形式化分析框架验证，这类工具会自动验证合约是否符合我们定义的规范3.发现某些情况下出现问题4.改代码解决问题一个真实案例：巫师决斗@CHZWZRDShttps://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/actScribble:https://docs.scribble.codesDafny:https://github.com/dafny-lang/dafny…用于检验正确性的验证器CertoraProver:https://docs.certora.com/en/latest/index.html…SoliditySMTChecker:https://github.com/ethereum/solidity…solc-verify:https://github.com/SRI-CSL/solidity…KEVM:https://github.com/runtimeverification/evm-semantics…
