I talk about separation kernels a lot as being strongest, building block for secure systems. This is paper that invented the concept. The main innovation was separating mechanism from policy. One thing that might surprise programmers is how they want distributed systems to be more like sequential systems for predictability whereas he wanted a sequential/monolithic system to be a distributed system for security. In any case, the separation kernels did well during NSA pentesting (i.e. INTEGRITY-178B), seL4 was verified down to the binary, and Muen was less affected by Meltdown/Spectre IIRC.
Although beware their zealous marketing, I'm posting INTEGRITY-178B link for architectural details and certification data since they're representative of high-assurance security.
