5.4 智能合约形式化验证

软件的形式化验证用于确定程序是否按照规范行事。一般使用某种具体的规范语言来描述函数的输入输出应该如何相关，并基于此证明程序的输入输出的相关性。

智能合约需要形式化验证。第一，智能合约一旦上链不可改变，因此编程漏洞变得不可接受；第二，智能合约是完全公开访问的，这提供了开放性和透明度，也使其成为黑客攻击目标。形式化验证是减少软件漏洞和攻击风险的强有效的方法，与传统方法（测试、同行评审等）相比提供了更高的正确性保证。

目前以太坊智能合约的形式化验证较难实现，因为以太坊虚拟机EVM不针对第三方提供测试，目前以太坊基金会仅使用机器辅助逻辑推理验证合约所需的工作量。如果要实现以太坊智能合约的形式化验证，需要彻底改革以太坊虚拟机EVM使其更容易进行形式化验证，或者建立全新的语言和虚拟机系统来支持形式化验证。但无论哪种选择，都需要制定形式化验证库和标准。