As a reminder: Millions of LoCs that run in supervisor mode. This is what Linux is.

It is not possible to fix all the bugs. This is simply not doable.

The solution has to be fundamental.

The microkernel multiserver system architecture, with a formally verified microkernel. Nothing else can guarantee enforcement of anything.

In practice, this is the same as saying seL4[0], because there are no alternatives.

Related: The seL4 summit 2026 vids are finally up[1].

0. https://sel4.systems/

1. https://www.youtube.com/playlist?list=PLd7rrADYxxQQ