The standard objection to microkernels is IPC cost. The cost is real, and it is where the discussion usually stops. That is the problem.
What you're buying is a fault boundary around a driver, and a monolithic kernel can't sell you one at any price, because a driver bug is a kernel bug by construction.
The structural claim¶
In Linux, a device driver runs in kernel address space with kernel privileges. There's no boundary to cross because there's no boundary there at all. A null dereference in a driver is a kernel oops; memory corruption can corrupt anything it likes.
This isn't an argument about code quality. You can write excellent driver code and the structural property doesn't budge. Drivers are also where the largest volume of kernel code lives and where the least-reviewed code lives, an uncomfortable combination on anyone's reading.
Put the driver in its own address space and a fault takes down the driver. A supervisor restarts it; the system carries on.
What the proof says¶
seL4's functional correctness proof gets cited loosely, so to be precise about it: the C implementation is proven to refine an abstract specification, with no unproven gap between the two. It doesn't mean "no bugs", because a specification can specify the wrong thing. It means the implementation and the specification provably agree.
That holds across Arm 32-bit, AArch64, x86-64 and RISC-V 64-bit, AArch64 having reached parity on functional correctness (seL4 Summit 2024). The MCS configuration now has a functional correctness proof on 64-bit RISC-V, completed by Proofcraft in June 2026 and shipped in seL4 16.0.0 (seL4 news); the AArch64 port of that proof is in progress.
On the 32-bit Arm configuration the proof also covers integrity and confidentiality above functional correctness, which is the part that lifts it out of academic curiosity. Confidentiality there means non-interference between the domain scheduler's domains, not between arbitrary threads. The other architectures have functional correctness alone; the stronger properties are not verified there.
Where the cost lands¶
The useful question about IPC isn't what one round trip costs. It's how often you hit the path.
A few thousand calls a second against a microsecond-scale IPC is noise. A million calls a second is the design. So the engineering work in a microkernel system is almost all batching: making the interface coarse enough that you rarely cross the boundary. That's the same optimisation as any RPC boundary, and a design constraint rather than a tax.
The open question is the sizing one, and it is answerable: on a named part, at a named kernel version, what does the IPC path cost against the equivalent syscall, and at what call rate does the batching argument stop holding? That measurement decides the architecture for a whole class of embedded system and we have not taken it on our own hardware. It is on the bench list, with the part number and the command, and no numbers appear here until it is.
What a verified boundary makes possible¶
The structural property changes what can be built and certified.
Take a car. A modern vehicle carries dozens of controllers because the infotainment stack cannot be allowed near the braking logic, so they get separate silicon, wiring and suppliers. With a verified separation kernel underneath, one processor can host the instrument cluster, the entertainment system and a safety function, isolation proven rather than asserted. That removes boxes, weight, wiring and cost from every vehicle built, and the same reasoning applies to avionics, industrial controllers and medical devices.
The certification effect is bigger than the hardware saving. Today, changing anything in a safety-certified system means re-arguing the safety case for the whole box, because nothing structurally prevents one component affecting another. With proven isolation you argue about one partition at a time. That is the difference between a device that gets a security update and one that does not, which is why so much safety-critical equipment in the field runs software nobody has touched in a decade. Proven separation is how you patch an infusion pump.
It also buys survivability where there is no staff and no second chance. A driver fault a supervisor can restart is a system that can sit in a substation or a satellite and keep going, which spacecraft software has historically bought with redundant hardware instead.
Where it falls down¶
- Driver availability. Linux's enormous driver tree is its real moat, and a microkernel hasn't got one. For most hardware that settles the argument.
- Shared-memory-heavy workloads, where the batching argument doesn't apply because the data is fine-grained.
- Developer familiarity. The pool of people who can debug a microkernel system is far smaller.
Those explain why Linux won the general case. None touches the structural claim, which is why microkernels keep winning where a driver fault is unacceptable: avionics, automotive, secure enclaves.
In the end, verified systems come down to the licence on the proof. seL4 is open source, and so are its proofs. That combination is unusual and the thing to protect. A published proof can be inspected, built on, ported and argued with by anybody, so a four-person company can ship on a formally verified base without employing a proof engineer: the expensive artefact has already been made and given away. That redistribution happened because the work was publicly funded and published.
The alternative model is already common here. Commercial separation kernels are certified to the relevant standards and sold per unit with the evidence package under NDA: you get a certificate and a binary. You cannot read the proof, port it or verify the claim yourself, and your safety argument depends on a document you are not allowed to show anyone. Same technology, opposite ownership.
Watch where the funding points. Much of the serious verification work in this field runs on defence research money. That is how it gets done at all, and it comes with a preference for the results reaching some people rather than everyone. The optimistic case is that proofs are artefacts and artefacts get published. The pessimistic one is a verified trusted base that is export-controlled while the open one stays a research kernel. The difference between those futures is licensing decisions being taken now by people not thinking about it hard.
Here at AxisOps we would build on the verified base we can read, and not for ideology. A safety case resting on a proof you are forbidden from examining has swapped one trust relationship for another and charged you for it. Verification converts a claim into something checkable; a proof under NDA converts it back.
The price of enforcing the boundary¶
The microkernel is the oldest approach to isolation and the only one where the boundary is enforced by hardware. Everything newer, eBPF and WASM included, is an attempt at a comparable guarantee without paying for it on every crossing.