This paper introduces the technical foundations of operating system verification theory, language, and tools, and elaborates new verification methods and concepts such as the verification path, refined relationship verification and largescale verification. The research content, verification methods, main contributions, and latest developments of multiple operating system verification projects are compared and analyzed. Meanwhile, this study also analyzes the problems in the process of operating system verification and believes that the high cost of verification and the limitations of verification tools are the key factors that restrict the formal verification of operating system. With the improvement of verification tools, frameworks and theorem libraries, new technologies such as deep learning have been improved and applied, thus more security properties of the operating system can be formally verified.