Compared with original microkernels, L4 greatly improves performance and flexibility and is widely used in various fields. The correctness and reliability of the operating system kernel play a decisive role in the stable operation of the system. This study presents formal specifications and verification for thread management, a key mechanism of L4. First, a safety specification is developed to describe safety properties, a standard L4 API specification is reused to define functional correctness, and an implementation specification based on the C++ source code is automatically generated. To alleviate the significant differences between the requirement specification and the implementation specification, an intermediate specification is introduced. The first two specifications are formalized in Isabelle/HOL, and the latter two are expressed in Python. The consistency among these specifications is guaranteed through refinement proofs, such as interpretation and the establishment of forward simulation. During the proofs, interactive verification and Auto-active verification are integrated, which improves the level of automation while reducing manual proof obligations. Eventually, three issues that violate correctness and safety properties are identified in the source code, and solutions are proposed for these issues.