So here is how it actually works with formal security audits, for example with an OS certified to EAL6 (Semiformally Verified Design and Tested). The OS vendor

So here is how it actually works with formal security audits, for example with an OS certified to EAL6 (Semiformally Verified Design and Tested). The OS vendor produces a boot loader and a simple task switcher that can pass messages. This is somewhat badly proven to be free of bugs. It's unimpressive because there is almost no code or functionality. Things like filesystems and TCP/IP stacks are full of security holes. None of that counts. All that buggy code gets linked into the user's app. Practically speaking, the app serves as a kernel without memory protection and the super-secure (Verified! Proven!) task switcher serves as a hypervisor. OK, so maybe nobody can hack into the simple task switcher that is supposedly an OS but actually a hypervisor. The big fat juicy app, containing most of a kernel, is as secure as VxWorks 5 or MacOS 9. It's not a good sign if you need to copy-and-paste the code for an old BSD network stack into your app. Maybe the theory is different, but in actual practice the above is really how the world of secure microkernels gets stuff done.