Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel

Abstract OpenHarmony LiteOS-M, a preemptive operating system (OS) kernel for the Internet of Things (IoT), is widely deployed in safety-critical domains, such as aerospace and transportation. As a rigorous method to assure software safety, formal verification has been applied to OS kernels in industry. However, entirely verified kernels with large codebases are rare, since such verification is typically performed within interactive theorem provers, requiring substantial human effort. In this paper, we present the functional correctness verification of LiteOS-M. First, to improve verification efficiency, we design a formal verification platform, Smart Verifier. The platform employs an annotation-based verifier as the front end, while the back end integrates Z3 and Rocq, combining automatic and interactive theorem proving techniques. Second, we tailor two verification methods, expressing program refinement as standard Hoare logic triples and modeling concurrency through state transition systems, to utilize the platform for verifying LiteOS-M. Our verified LiteOS-M kernel consists of 17,000 lines of C. During the code review and verification, we find a total of 17 bugs, all confirmed and fixed by developers.