ManualsThe Manuals section has the current defining L4 API specification document. For reference, previous specifications are available as well.
InternalsInside L4/MIPS is an attempt to document the internal structure of L4 and its operations. It is based on the Version 2 L4/MIPS, kernel version 79 (February 1999). The document is meant as an aid in teaching operating systems internals, and as a guide for kernel implementors. While the actual code discussed is very specific to the MIPS processor, much of the overall structure and logic of L4 is quite similar across platforms. The most serious limitation of the document is that modern L4 versions are almost fully implemented in higher-level languages, while the version on which this document is based is about half assembler. This means it is written at a (now) unecessarily low level. Unfortunately no-one has yet found the time to write a similar document for L4Ka::Pistachio.
UNSW's Advanced Operating Systems course provides an in-depth coverage of microkernel concepts, design and implementation issues (besides other advanced-level material). It has been running in essentially the same format since 1999, and variants of it have been adapted by a number of other universities. The lecture slides of the first few weeks contain a general introduction to microkernels, and a detailled coverage of seL4 concepts and mechanisms. It is accompanied by a project where students build a complete OS on top of seL4.
There also exists a lecture in Dresden on Microkernel Construction, which was inspired by a former Karlsruhe lecture, and focuses on Dresden's implementation Fiasco.OC. Additionally, a user land lecture, Microkernel-Based Systems, is held in Dresden.
The performance page summarises 20+ years of L4 performance data across kernels and architectures.