On: The seL4 microkernel

[tambourine_man]

There was a project way back when to port Darwin to L4: http://www.ertos.nicta.com/software/darbat/

along with the accompanying rumor that Apple would be “lifting” Mach's layer in XNU to run on top of L4. That was before the iPhone, of course.

I was always fascinated by the talks of L4 being specifically designed to avoid scrubbing your L1/L2 cache on operations such as IPC.