1 files changed, 35 insertions, 0 deletions
diff --git a/microkernel/l4.mdwn b/microkernel/l4.mdwn
new file mode 100644
index 00000000..45929842
--- /dev/null
+++ b/microkernel/l4.mdwn
@@ -0,0 +1,35 @@
+[[!meta copyright="Copyright © 2004, 2006, 2007, 2008, 2010 Free Software
+Foundation, Inc."]]
+
+[[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable
+id="license" text="Permission is granted to copy, distribute and/or modify this
+document under the terms of the GNU Free Documentation License, Version 1.2 or
+any later version published by the Free Software Foundation; with no Invariant
+Sections, no Front-Cover Texts, and no Back-Cover Texts.  A copy of the license
+is included in the section entitled [[GNU Free Documentation
+License|/fdl]]."]]"""]]
+
+The [*L4* microkernel](http://l4ka.org/) is an attempt to create a very small
+high performace core which provides basic memory management, task and context
+switching, and little else.
+
+[L4Ka Pistachio Home](http://l4ka.org/projects/pistachio/).
+
+See [l4.verified](http://nicta.com.au/research/projects/l4.verified) for work
+on formally verifying an L4 microkernel.
+
+  * {{$sel4}}
+
+There was a GNU/Hurd [[history/port_to_L4]], which is now stalled.
+
+
+[[!ymlfront data="""
+
+sel4:
+
+  "G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin,
+  D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and
+  S. Winwood.  seL4: Formal verification of an OS kernel.  In Proceedings of
+  the ACM Symposium on OS Principles, Big Sky, MT, USA, October 2009."
+
+"""]]