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
