As far as I know, the state of the art in efficient microkernels is the L4 family: https://en.wikipedia.org/wiki/L4_microkernel_family https://en.wikipedia.org/

As far as I know, the state of the art in efficient microkernels is the L4 family: https://en.wikipedia.org/wiki/L4_microkernel_family https://en.wikipedia.org/wiki/L4_microkernel_family and you can find some real meat about how they've been so successful in this paper: http://www.nicta.com.au/publications/research-publications/?term=l4&term_field=title&pageno=3&pid=6930 http://www.nicta.com.au/publications/research-publications/?... One big thing: seL4 has been formally proven, down to the binary gcc emits for it. Ah, I see these slides, as I'd expect from an Australian source, start taking about L4 on slide #44.