seL4 is really cool; I was just looking at and the other L4 family / derivatives for µkernel ideas and trends.
More links:
- https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
- seL4: Formal Verification of an OS Kernel (2009) [pdf paper] http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
- l4v (seL4 proofs git repo) https://github.com/seL4/l4v