seL4 having a proof of correctness does not mean all microkernels do. In fact, seL4 is the only microkernel that has a proof of correctness. If you build on top of it in the microkernel way, you quickly find that it is not performant. That is why NT and XNU both abandoned their microkernel origins in favor of becoming monolithic kernels.
I’ve seen this argument play out many times. I believe the next line is: “QNX proved that micro kernels can be fast given clever message passing syscall design.”
“I remember running the QNX demo disc: an entire graphical operating system on a single 1.44MB floppy! Whatever happened to them?”
“They got bought by blackberry, which ended as you’d expect. QNX had a lot of success in automotive though.”
“Nowadays Linux and Android are dominant in new cars, though, proving once and for all that worse is better.”
Also an illustration how an open-source solution, even if technically inferior, would displace a closed-source solution, even if technically superior, unless there is a huge moat. And huge moats usually exist only in relatively narrow niches.
It turns out that success is composed of 90% luck, 10% marketing, and 5% talent/technical advantage. A rhetorical question: how do you entice people to turn a movement into a revolution when it isn't likely the movement will succeed?
Another rhetorical question: out of luck/marketing/technical advantage, which one is contributing the most to the extra 5% out of 105% of all the components success can be attributed to?
NT and XNU never had microkernel origins - Cutler explicitly refuted this at a conference in the early 1990s (if anyone remembers which, kindly share) and NeXTSTEP forked Mach at version 2.5, which was not a microkernel (see https://cseweb.ucsd.edu/classes/wi11/cse221/papers/accetta86...). XNU retained this monolithic architecture (as did Tru64 and other systems that trace their heritage to Mach prior to its version 3).
Various sources state that they rebased to OSF Mach Kernel 7.3, which was based on Mach 3 and parts of Mach 4. The OSF MK ancestry of macOS XNU can still be seen in paths:
This is quite a ship-of-Theseus problem. Steve Jobs hired Avi Tevanian to work at NeXT on the Mach kernel, and later brought Tevanian to Apple; he was still working on the Mach/Darwin kernel as late as the first iPhone release. There is a reasonable argument to be made that the OSF kernel is actually the derivative, by default.
As far as I can tell (this isn't gospel, just something I've inferred as the only reasonable explanation from comparing the codebases), Apple reconstructed a Mach 2.5 style kernel, like NeXTSTEP had, from fresh codebases (OSF Mach and 4.4BSD-Lite2), perhaps because 4.3BSD was still encumbered at the time.
The Darwin 0.1 and 0.3 releases contain the old kernel, derived directly from NeXTSTEP, and that's the direct derivative of Mach 2.5. The later XNU appears to be a reconstruction of that kernel with unencumbered code and that's also when IOKit replaced DriverKit.
In more recent interviews Cutler has been firm that the NT kernel was designed pragmatically, a view that Tevanian also evidently later adopted, as evident with the great wheel of incarnation that Darwin went through on the road to XNU, although I'm not sure Tevanian ever stated his perspectives on this matter publicly. Neither of these systems were ever true monolithic kernels in the Linux or Unix sense—at all times they both had some measure of sandboxing between e.g. driver code and the scheduler—rather sitting somewhere between.
True microkernels are, alas, more of an ideology than a practical reality, as the long-suffering GNU/HURD team discovered; Tanenbaum has been clear that the MINIX/NetBSD experiment was more about principles than performance. That said, certainly many hypervisors have attained success with configurations that coincidentally happen to be the same footprint as a microkernel.
From talking with some people who were witnesses to earliest days of Hurd (but not involved in the project), the real problems of Hurd were social not technical - if anything, OSF/1 & NeXTSTEP succeeding from similar code base (for some value of) points that it was possible to do it.
The story goes that the early days were dominated by some ridiculously bad project management that makes Cathedral and the Bazaar era "Cathedral" a nice and well maintained project.
Most importantly, GNU Hurd lacked the "ecological niche" to drive work towards it because it couldn't deliver enough, just like lack of information about 386BSD led to Linux (Linus explicitly said that if he had known about 386BSD, he would have worked on it and maybe forked it)
The hypervisor/microkernel boundary has blurred, and commercial success for microkernels is more or less as hypervisors, e.g. OKL4 is widely used in mobile devices[0]. And Tanenbaum's Minix is used for the Intel Management Engine. I don't know the details with HURD, but I don't think it is mainly suffering from "inherent" or "nearly-inherent" (strongly associated) problems of microkernels. The main cost of microkernels is developer effort and likely performance overhead.
NT and XNU never had microkernel origins - Cutler explicitly refuted this at a conference in the early 1990s
Interestingly, the Tanenbaum–Torvalds debate had Tanenbaum claim otherwise at the very start:
The alternative is a microkernel-based system, in which most of the OS runs as separate processes, mostly outside the kernel. They communicate by message passing. The kernel's job is to handle the message passing, interrupt handling, low-level process management, and possibly the I/O. Examples of this design are the RC4000, Amoeba, Chorus, Mach, and the not-yet-released Windows/NT.
NT incorporates a client/server model, like a microkernel, but isn't a "pure" microkernel like Mach. This gives rise to the 'hybrid kernel' term, which Linus dislikes.
Wikipedia has a decent depiction of the hybrid structure, but quoting from the NT Design Workbook:
> This specification describes the kernel layer of the NT OS/2 operating system. The kernel is responsible for thread dispatching, multiprocessor synchronization, hardware exception handling, and the implementation of low-level machine dependent functions.
> The kernel is used by the executive layer of the system to synchronize its activities and to implement the higher levels of abstraction that are exported in user-level API's.
NT in Windows 11 has very little to do with the monolithic kernel story that keeps being repeated.
Not only did the graphics stack moved again back into userspace, there is now a complete userspace drivers stack, and VBS (Virtualization-based security) for several kernel components that run on their mini Hyper-V island, talking via IPC with the rest of the kernel.
Likewise on XNU land, Apple has started a crusade already a few years ago, to move all kexts into userspace, no more drivers in the kernel beyond the ones Apple considers critical.
In both cases, they never were a pure monolithic kernel, due to the way walls were introduced with kernel level IPC to talk across modules, instead of straight function calls.
> seL4 is the only microkernel that has a proof of correctness
ProvenCore (https://provenrun.com/provencore/) has a proof that covers correctness (memory safety, and more generally absence of UB, termination, etc.), functional properties (e.g. the fork() system call is a refinement of an abstract "clone" operation of abstract machines), and security properties (memory isolation).
