The growing need for highly reliable system software has drawn widespread interest in formal methods in the industry. This paper presents an overview of the mainstream formal methods and analyzes the current research status in this regard. Then, it describes the application of formal methods in the design and implementation of operating systems, compilers, synchronization primitives, file systems, database systems, and distributed consensus protocols. On this basis, it summarizes the experience learned in applying formal methods to system software and discusses potential challenges from the theoretical and engineering aspects. Finally, it gives some suggestions on how to address these challenges.