FWIW, I would not trust seL4 on x86. Last time I checked, seL4’s interaction with the x86 architecture was not formally verified and looked quite buggy. Even a

FWIW, I would not trust seL4 on x86. Last time I checked, seL4’s interaction with the x86 architecture was not formally verified and looked quite buggy. Even a microkernel has three things that form part of the TCB: the part that interfaces with the even-lower-level stuff (interrupt and exception handlers, paging, memory model, etc), the interface it provides to its clients (syscalls and whatever it provides via syscalls), and the code that glues the first two parts together and implements the microkernel’s internal logic. The latter two, in seL4, are straightforward and formally verified. The former, on x86, not so much. AIUI, the situation on ARM is likely better.