The paper discusses more fundamental issues than just x86 architecture: * Usermode drivers need to be formally verified to prevent malicious DMA. Adding IOMMU/

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.