Modern operating systems consist of millions lines of low-level code, which is hard to understand, maintain, and validate. In this talk I will advocate the rigorous approach to OS design as a way to overcome the problem. I argue that the time has come to re-think the OS design based on a solid mathematical foundation. This long-sought vision is finally becoming feasible due to recent advances in programming languages, model checking, and interactive theorem proving. I will outline a high-level methodology for rigorous OS design, consisting of three components: (1) a theoretical foundation for formal reasoning about OS behaviour at a level of abstraction much higher than C code, (2) a software ecosystem, consisting of domain-specific languages and tools that provide a programmer-friendly interface to the theory, (3) OS implementation, built and verified on top of this ecosystem. As a concrete instantiation of this methodology, I will present the Termite project, which has developed the first tool for automatic synthesis of correct-by-construction device drivers. In Termite, the driver behavior is formalized in terms of the discrete control theory and is automatically synhtesized using controller synthesis techniques. I will show how the connection to the control theory enables efficient formal reasoning about complex low-level software. The talk will conclude with a brief demo of Termite.