Yeah in theorem provers usually the opposite is true: "We want to put as little stuff as possible in the kernel because that's the part we need to verify by hand"
That counts especially for accidental bugs and denial of service. To make a userland bug exploited adversarially not impact the rest of the system requires more hardening of the kernel.
Say it with me - there's no practical difference.
You can compartmentalise further.
Modern processors even give you these 'rings' to help with the hardware side of that, if you want to.
They differ in how easy a fix is to develop and roll out, and what the blast radius is.