Hyperkernel explores a push-button approach to building provably correct OS kernels.
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), Oct 2017. [pdf] [slides]
Dylan Johnson. Porting Hyperkernel to the ARM Architecture. Technical Report UW-CSE-17-08-02, University of Washington, Aug 2017. [pdf]
The source code is hosted on Github at https://github.com/locore/hv6/.