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