- Have you considered using a micro kernel based host like seL4, similar to what Genode does (at least as I understand it)?

Yes. I don't know all that much about microkernels, but I have spoken to some microkernel experts. My understanding is that all the required parts are not yet in place to be able to use a microkernel as the host in a system like Spectrum. I am, however, trying to design the system so that the host system is responsible for as little as possible, and therefore hopefully making it possible to transition to a microkernel later should that look feasible. In principle, the host system should do little other than running virtual machines. Ideally, most hardware interation could be delegated to VMs. This would make it possible to have a very tiny host kernel through disabling most kernel configuration options. The left over code should be just what is critical to run VMs. The paper "A Linux in Unikernel Clothing"[1] compares a minimally-configured Linux kernel to several popular unikernels (not microkernels), with very promising results. It is focused on tiny kernels for single-purpose virtual machines, but I think it contains a lot of relevant insight for all levels of the Spectrum stack. [1]: https://dl.acm.org/doi/pdf/10.1145/3342195.3387526

- Have you considered gVisor [1] for lightweight compartmentalization?

Yes. The main problem I see with gVisor is that it is designed to be run from a full-featured host system. For example, gvisor doesn't provide file system implementations. Instead, it expects to proxy through a file system existing on the host. In Qubes, and hopefully in Spectrum, the host system doesn't have any knowledge of VM file systems, to keep the host as separated from the activities of VMs as possible. There may still be a place for gVisor in Spectrum -- for example, it could get a shared file system from a separately virtualized kernel. For now, though, one VMM is enough to be going on with. :)

- Have you considered reusing stuff from the Whonix project?

Yes. My understanding is that the main thing that Whonix provides is full system images for workstation and gateway machines. We probably wouldn't want to use these directly in Spectrum, because it would go against the principle of configuring the entire system with Nix. However, there will likely be lots of work in Whonix (configurations and so on) that can be reused to similar ends in Spectrum.