The failure of a safety-critical system can cause serious consequences, and it is very important to ensure its correctness. The space embedded operating system is a typical safety-critical system. In the design of its memory management, it must ensure its efficient allocation and deallocation, and the occupancy of system resources is minimizedat the same time. In the traditional software development process, centralized testing and verification are usually carried out after the entire software development is completed, which will inevitably cause uncertaindevelopment. Therefore, this study combines the formal verification method with the three-tier development framework of "demand-design-implementation" in the field of software engineering, and ensures the consistency of each level through the method of layered transfer verification. First, starting from the demand analysis of the demand level, the idea of formal proof is introduced to prove the correctness of the logic of the demand level, which can better guide the design of the program. Second, verification at the design level can greatly reduce the error rate of the development code, and prove the correctness of the call logic between the design algorithm and the function that needs to be implemented. Third, at the code level, it is needed to prove the consistency of the implemented code and the functional design, and prove the correctness of code. Using the interactive theorem proving auxiliary tool Coq, this study takes the memory management module of a domestic space embedded operating system as an example, to prove the correctness of the memory management algorithm and the consistency of demand, design, and code.