SEL4 would be a better choice because it is formally verified, there is a much smaller chance of vulnerabilities in SEL4 vs Xen because of this.

From the above link:

What about safe languages and formally verified microkernels?

In short: these are non-realistic solutions today. We discuss this in further depth in our Architecture Specification document: https://www.qubes-os.org/attachment/wiki/QubesArchitecture/a....

Interestingly enough they only mention it being unreasonable for x86, it would be interesting to see SEL4 supported for ARM (of which SEL4 already has a verified kernel for).

The paper discusses more fundamental issues than just x86 architecture:

* Usermode drivers need to be formally verified to prevent malicious DMA. Adding IOMMU/SMMU to the microkernel will complicate the current proofs.

* All user processes that manage resources, like filesystem, network and memory management, must also be formally verified. These are currently unproven.

See also: https://github.com/QubesOS/qubes-issues/issues/4318.