Hm, if you're making the underlying hardware slower, don't you want the kernel to be even faster though?

Not when using hypervisor type 1.

Why not? Hypervisor type 1 has less overhead, but it's still not quite the same as running directly on the box. I don't think micro kernels would replace those anyway. To be honest, I don't even really see the connection between running most of the kernel in user space and allowing concurrent systems to run in the same hardware.

seL4 with its VMM is a better hypervisor architecture than, say, Xen.

Xen is unfortunately large, and the full hypervisor runs privileged.

With seL4, VM exceptions are forwarded to VMM, which handles them.

From a security standpoint, a VM escape would only yield VMM privileges, which are no higher than that of the VM itself. This is much better than a compromise of Xen, which would compromise all VMs in the system.

Makatea[0] is an effort to build a Qubes-like system using seL4 and its virtualization support. It is currently funded by a NLNet grant.

0. https://trustworthy.systems/projects/TS/makatea