I find the L4 Microkernel [0] pretty interesting. The goal of L4 is to make the microkernel architecture performant by making IPC fast. They did this by making the implementations processor dependent; they wrote the IPC code in optimized assembly. A variant [1] of it is actually commonly used in baseband processors. See this paper [2] for a good overview.

[0] - http://os.inf.tu-dresden.de/L4/overview.html

[1] - http://www.ok-labs.com/products/okl4-microvisor

[2] - http://homes.cs.washington.edu/~bershad/590s/papers/towards-...