定义好安全性之后，我们验证的对象是什么？这里可以分为模型级别验证和代码级别验证。但是不管怎么验证，我们需要对验证的代码写出「规范」，从上面的例子延伸：

Solidity 开发语言里面有一个 方法 A(i)，输入 i，输出 B;

形式化验证就是，根据方法 A(i) 产生另一个方法，也输入 i，得到 B。这就证明了方法 A 是 OK 的。

这就是在验证一个行为满足规范。

那么这个验证过程，可以是自动化的，半自动化的，也可以是人工的。但是形式化验证很快会面临一个很困难的新问题：如果代码量很大怎么办？如果代码会频繁改动怎么办？

这是过去二十年，形式化验证领域的研究热点，就是如何把代码拆成很多的模块，然后实现验证的模块化，这里面的理论难度深不见底。

这里我来谈谈最后一个形式化验证的难题，这就是工具悖论。假如，我们把代码验证完了，借助了一个工具。那么问题来了，这个工具的安全性怎么来保证？为了验证这个工具，我们又需要一个新工具。

有一类形式化验证，会产生「Proof Term」，也就是具体的验证过程的表达。

定理 1：对任意的环境 Env，对所有的输入 I，程序 Env |- P(I) 运行得到一个执行行为序列 [B0, B1, B2 ..... Bn]，forall i, Safe(Bi)。

证明：

…「Proof Term」（略）

证毕。

也就是中间那个非常庞大的证明过程，它可以摆脱对验证工具的信任依赖，类似于区块链中我们不需要信任矿工一样。我们可以借助各种先进的验证证明产生工具，只要他们能产生对的证明，他们本身是否安全不重要，这是一种很本质的新的去中心化技术。

形式化验证是银弹吗？

并不是。

挑战一：成本很高，需要很多的智力投入。

挑战二：需要理论上的重大突破，提高逻辑的自动推理能力。

挑战三：一方面我们需要更复杂的 DeFi 功能！另一方面，复杂理论的验证方法更难。

验证技术与技术创新存在一个赛跑，目前来看，验证技术远远落后于技术的发展，Fuzzing，符号执行，人工审计，动态监控，应急预案，这些传统的技术需要和先进形式化验证技术一起使用。

主持人：在未来的 3-5 年内，我们有没有可能通过 Etherscan 等区块链浏览器上一个通过形式化验证的标记来确认该智能合约的安全性？

郭宇：对于简单的智能合约是很有希望的，比如 ERC20 的 token 合约 。但是对于超过 2000 行的智能合约，难度就会加大很多。其实我们不能仅关注「打勾」，而是需要看形式化验证的那个最终定理是否是有意义的，或者说是否 sound。并且可能出现今天打了勾，明天就发现问题，需要取消，所以其实需要制定标准。这个未来需要一个社区，有专家，有用户，有黑客，大家一起来建设，3 年有点短，5 年也许有希望，建议采取学术界的同行评议机制。 (责任编辑：admin)