[snvzz]

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