形式化验证方法是智能合约进行确定性验证的有效手段，通过形式化语言把智能合约中的概念，判断和推理转化成智能合约模型，可以消除自然语言的歧义性和不通用性，进而采用形式化工具对智能合约建模、分析和验证，进行语义一致性测试，最后自动生成验证过的合约代码.如图2所示，本节将近年来基于形式化验证智能
