seL4

The seL4 microkernel is the world's first operating system with a formal, machine-checked proof of implementation correctness. It is still the most comprehensively verified OS kernel, including proofs of security enforcement. It is also the only formally-verified capability-based kernel, and yet the world's fastest microkernel. It is the best base on which to build security- and safety-critical systems, especially for embedded and cyberphysical systems.