[ryao]

A microkernel could go into the kilobyte range too. seL4 is definitely in that range. The smallest Linux kernel bzImage that I ever compiled was something like 570KB, so embedded Linux might be able to reach that range too. That would of course include an application. The QNX demo likely could reach such sizes too if most of the things in it were removed. For those that are unaware, QNX is a microkernel based system.

[eru]

seL4 doesn't provide very much to the programs, does it? I think it closer in spirit to Xen than to the linux kernel?

[ryao]

The Xen hypervisor uses a microkernel architecture. A kernel could implement a userland (e.g. traditional UNIX), a VM interface (e.g. KVM) or nothing at all (e.g. a unikernel). My point is that unikernels do not have a monopoly on small sizes and they are not worth mentioning as an advantage.