TL;DR: Changes KVM on ARM to run a tiny verifiable codebase in EL2 (derived from the original KVM code?), and run the rest of the kernel in EL1, then uses stand

TL;DR: Changes KVM on ARM to run a tiny verifiable codebase in EL2 (derived from the original KVM code?), and run the rest of the kernel in EL1, then uses standard formal verification techniques on that tiny EL2 component. In a sense, it changes KVM into a Type 1 hypervisor in order to reduce the verification needed to a manageable level. Neat, reminds me of rtlinux, using a Linux module to boot a microkernel with a reduced TCB and more useful semantics in some cases than a full Linux kernel.