Comment by nickpsecurity

Exactly. The question is how mature they are and what you're implementation language would be. The MILS security people have been doing this for over a decade with the effective approach of combining separation kernels, user-mode OS's for GUI/legacy, and critical stuff running right on the kernel. Relative to MirageOS, several vendors developed special runtimes for Ada and Java to leverage their safety properties without the complexity of a standard runtime.

So, it's a proven approach that could be implemented in GenodeOS and probably easier given others were bare-bones.