智能合约的形式化验证方法研究

Formal methods are widely used in safety-critical software systems and have effective mathematical-based verification methods, while smart contracts belong to safety-critical codes.Using formal methods to verify smart contracts has become a popular research topic.This paper has conducted researches and analysis on 47 typical related papers since 2015 and carried out detailed classification research and comparative analysis on technology, as well as the formal methods, languages, tools and frameworks used in the formal verification of smart contracts overview.Research shows that theorem proving technique and symbolic execution technique have the widest scope of application, can verify the most properties and are involved in many basic frameworks.And the runtime verification is a new lightweight verification technology, still in the exploratory stage.From this, we have listed some key issues such as automatic verification of smart contracts, conversion consistency, trust in formal tools, and evaluation criteria for formal verification.This paper also looks forward for the future research direction on the combination of formal methods and smart contracts.For attracting more valuable ideas and promote the research in the field.