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.