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.