Real-time Operating Systems (RTOSs) are widely used to design and develop embedded safety critical software applications. Such applications have to be fault tolerant, deterministic and meet stringent safety standards which include several functionality-related real-time requirements. The applications rely on, and use several features of the underlying RTOS to satisfy these design requirements. Real-time operating systems provide kernel APIs and scheduling algorithms to cater to many of the safety requirements. We will discuss our experience of formally verifying several safety critical requirements of one such indigenous RTOS that has time and space partitioning features and is being used by the Indian avionics industry.