The Xen "microkernel" is unfortunately bloated. seL4 is much smaller and runs VMM as an isolated unprivileged task. VM exceptions are all handled by VMM. A VM

The Xen "microkernel" is unfortunately bloated. seL4 is much smaller and runs VMM as an isolated unprivileged task. VM exceptions are all handled by VMM. A VM escape would still be confined in VMM, which has no higher capabilities than the VM itself. Capabilities are enforced by the formally verified seL4.