The L4 microkernel is an attempt to create a very small high performace core which provides basic memory management, task and context switching, and little else.
See l4.verified for work on formally verifying an L4 microkernel.
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the ACM Symposium on OS Principles, Big Sky, MT, USA, October 2009.
There was a GNU/Hurd port to L4, which is now stalled.
IRC, freenode, #hurd, 2012-08-02
<mcsim> If someone interested, there is a channel with lectures about Genode and L4: http://www.youtube.com/user/drsartakov?feature=watch