公有链的本质挑战之三

6月7日：（缺乏合约的形式化验证）
3：缺乏合约的形式化验证
智能合约的形式化验证仍然是一个未解决的巨大问题。首先，让我们通过「形式化证明（formal proof）」来理解「形式化验证（formally verify）」的意思。在数学上，「形式化证明」是一种数学证明，计算机可以通过基本的数学公里和推理规则（inference rules）来证明它。
在程序方面，形式化验证是一种判断程序是否能按预期运行的方法。具体的规约语言可以来描述输入和输出之间的函数关系。也就是说，如果在程序里声明了一个不变量，则我们应该证明这个声明的存在。
规范语言的一个例子是Isabelle，它是一种通用证明辅助，可以在形式化语言里表达数学公式，还提供了工具在逻辑运算上来证明这些公式。另一种规范语言是Coq，这是一种用来书写数学定义、执行算法和定理的形式语言。
对于编码在智能合约里的程序来说，为什么形式化验证十分重要？一个原因是智能合约是不可逆的，这意味着一旦将它们部署到主网络里，你就无法升级或修改它们。因此在部署和使用智能合约之前，需要保证一切都不会出错。而且，智能合约是可公开访问的，存储在智能合约里的内容对任何人可见；每个人都可以调用智能合约里的公开方法。这带来了开放性和透明性，但也会吸引黑客攻击智能合约。
无论你多么小心谨慎，写出一个没有bug和完全可信的智能合约都是十分困难的。此外，在以太坊上，由EVM指令的设计方式，验证EVM代码也很困难。因此在以太坊上很难找到一种形式化验证的解决方案。但无论如何，形式化验证都是一种减少bug和攻击的强有力手段。比起传统方法（如代码测试和同行审查），它在很大程度上可以保证正确性。我们急切地需要一种更好的解决方案。