Formal methods are techniques with mathematical foundations for specifying, developing, and verifying computer software and hardware systems. Their mathematical foundations lie in formal logic systems, consisting of formal languages, semantics, and proof systems. Formal methods have been increasingly applied in different stages of the lifecycle of a computing system with appropriate levels of rigor. This paper reviews the historic development of formal methods. Focusing on specification and verification, the paper discusses and introduces the state-of-the-art mainstream formal methods in details, including their theories, techniques, tools, and applications. It is also shown that the relation between formal methods and other fields of computer science. Finally, the opportunities, trends, and challenges of formal methods are forseen. Formal methods have made significant progresses and played crucial roles to guarantee the safety and security of computing systems. Now software is becoming a fundamental infrastructure, it is believed that formal methods will gain much wider applications, especially when they are used in combination with other theories and methods such as those in artificial intelligence, cyber security, quantum computing, and bioinformatics. Research to achieving such seamless combinations is, however, both challenging and important.