L4
L4 is a family of second-generation microkernels based on the original designs and implementations by German computer scientist Jochen Liedtke. Originally implemented as highly tuned Intel i386-specific assembly language code, the API has seen extensive development in a number of directions, both in achieving a higher grade of platform independence and also in improving security, isolation, and robustness.
Source Code and Reference Manual
The L4/x86 source code written in assembler and the reference manual can be found here: http://www.acm.uiuc.edu/white_papers/incoming/GMD/L4/