After Liedtke's passing, L4 research was continued in groups at UNSW (Gernot Heiser, formal verification -> SeL4) and TU Dresden (Hermann Haertig, Fiasco/L4Re,

After Liedtke's passing, L4 research was continued in groups at UNSW (Gernot Heiser, formal verification -> SeL4) and TU Dresden (Hermann Haertig, Fiasco/L4Re, focusing on real-time and secure systems). Genode (already mentioned in another comment) [1] came out of the TU Dresden group with some nice ideas around managing compartmentalized systems. Kernkonzept [2] is a startup commercializing the L4Re microkernel. [1] https://genode.org/ https://genode.org/ [2] https://www.kernkonzept.com/ https://www.kernkonzept.com/