However, it is still a boring type-2 hypervisor, just like bhyve, vmware or kvm; no real progress whatsoever.

I'm keeping an eye at seL4's VMM support, it looks promising, with the microkernel actually guaranteeing isolation, whereas the VMM runs with minimum privileges as a user process.