From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels? (2013)

Summary. Inter process communication (IPC) was on the critical path of microkernels like Mach. Traditionally, each IPC took roughly 100 microseconds and was considered a bit high. In 1993, Jochen Liedtke introduced the L4 microkernel and showed that IPC could be implemented 10 to 20 times faster. In the next 20 years, L4 developed a rich family of descendants and many lessons have been learned.

Lessons in design:

Lessons in implementation: