One thing that is much easier to do in a microkernel than in a monolithic kernel is build a machine-checked proof of correctness. This is not to say that this

One thing that is much easier to do in a microkernel than in a monolithic kernel is build a machine-checked proof of correctness. This is not to say that this cannot be done in a monolithic kernel, but the proof would have to extend to each device driver and service within the kernel, or at the very least, a large portion of the kernel would need to be disabled to bring the proof down to something that can be accomplished by a team of developers in a reasonable period of time. A complete proof of correctness in a microkernel based operating system can be done in parts. First, the microkernel itself can be formally verified. Then, the communication mechanism between components can be formally verified. Then, each service or driver can be formally verified with regards to the communication mechanism, and its own contribution to the system as a whole. As long as it can be proved that the system will still operate correctly with one or all of these services or drivers in an invalid (crashed) state, then some level of operation can be guaranteed. In a correct context (fault tolerant hardware, such as a well built embedded system), such a microkernel architecture could be designed, and proven, to be robust. The formal verification of seL4 is one example of this in practice. Now, could one do the same proof-by-parts with a well designed monolithic kernel? Probably. However, the stronger the division is between parts, the more like a microkernel the monolithic kernel would become, until it would make sense to take advantage of IPC mechanisms between the parts to simplify the mechanical proof. Hence, we sort of come full circle. While I appreciate both sides of this debate, I would rather run the risk of a slower but more correct system than a faster system that is harder to formally verify. This is not to say that all microkernel based operating systems are more robust than monolithic kernel based operating systems, but there is a growing subset of microkernel based operating systems that have been formally verified, and I'm quite happy about that.