Microkernels are often used in high-security/high-criticality use cases because the kernel's facilities are very limited and the surface area is very small (thus easier to reason about and assure). Most complex functionality is performed in isolated processes/tasks with known IPC boundaries (i.e. a random thing can't clobber or inspect the memory of everything else).

We build on top of seL4 for these reasons (among others).