智能合约形式化验证

形式化验证方法是智能合约进行确定性验证的有效手段，通过形式化语言把智能合约中的概念，判断和推理转化成智能合约模型，可以消除自然语言的歧义性和不通用性，进而采用形式化工具对智能合约建模、分析和验证，进行语义一致性测试，最后自动生成验证过的合约代码.如图 2所示，本节将近年来基于形式化验证智能合约的方法进行归类研究，认为大致可分为8种技术，并列出每种技术对应的论文数量.基于该分类方法，对每个技术进行对比研究。

目前常见的形式化验证方法主要可分为两类：演绎验证和模型检测。演绎验证主要基于定理证明（Theorem Proving）的基本思想，采用逻辑公式描述系统及其性质，通过一些公理或推理规则来证明系统具有某些性质。目前主要的演绎验证工具有：基于Manna-Pnueli证明系统的STeP（Stanford Theorem Prover）、TLV、机器定理证明器（ACL2、Coq、HOL、Isabelle、Larch、Nuprl、PVS、TPS）等。模型检测（Model Checking）方法的基本思想是通过状态空间搜索来确认合约是否具有某些性质。即给定一个合约（程序）P和规约ψ，生成对应于合约模型M，然后证明M╞ψ，即规约公式ψ在合约模型M中成立，这样就证明了合约（程序）P满足规约ψ。常用的模型验证工具有：SMV（Symbolic Model Verifier）、SPIN（Simple Promela Interpreter）、SDL（Specification and Description Language）、UPPAAL等。