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.
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....