Not only that, but seL4 [0] is a cool NICTA effort that's been ongoing for almost a decade now to produce a secure, machine-verified microkernel based on L4. It

Not only that, but seL4 [0] is a cool NICTA effort that's been ongoing for almost a decade now to produce a secure, machine-verified microkernel based on L4. It seems like there's lots of room for L4 and its children to occupy interesting spaces in OS design. [0] http://ssrg.nicta.com.au/projects/seL4/ http://ssrg.nicta.com.au/projects/seL4/