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.

L4Ka Pistachio Home.

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

IRC, freenode, #hurd, 2013-08-26

< Spyro> also
< Spyro> what's the basic difference between mach and L4?
< braunr> l4 is a nanokernel whereas mach is a hybrid with high level
  messaging and virtual memory services