Gernot Heiser

In 2009, the seL4 microkernel became the first ever industrial-strength, general-purpose operating system (OS) with formally proved implementation correctness. The seL4 team further added proofs that seL4 enforces the core security properties of integrity (2011) and confidentiality (2013), while also removing the assumption that the C compiler must be trusted (2013), and performed the first sound and complete worst-case execution-time analysis of a protected-mode OS (2011).

 The seL4 high-assurance microkernel has fundamentally changed the research community's perception of what formal methods can accomplish: it showed that not only is it possible to complete a formal proof of correctness and security for an industrial-strength operating system kernel, but that this can be accomplished without compromising performance or generality.

 The functional correctness proof of seL4 was at the time one of the largest, and has now outgrown any other formal proof, consisting of over 1 million lines across three ISAs. Remarkably, the proofs have been maintained over a system that evolved significantly in 13 years, with less than half of the original kernel code still in use, and significant new features added. This has given rise to a new discipline of proof engineering---the art of proof process modelling, effort estimation, and the systematic treatment of large-scale proofs.

seL4's real-world impact began with its open-sourcing (2014) and the DARPA HACMS (High-Assurance Cyber Military Systems) program, which was explicitly motivated by progress on seL4 and on the verified compiler CompCert. HACMS demonstrated seL4's ability to protect autonomous systems from cyber-attacks, which led to a re-assessment of formal methods in US defense, and to seL4's deployment into defense systems. Responding to the growing open-source community, the seL4 Foundation, created in 2020, enlists several companies that rely on seL4 in their products, especially autonomous cars. Today, a vibrant seL4 ecosystem is forming, enabling verification for real systems where security and safety are critical.