Performance is the major flaw with microkernels that have prevented the half-dozen or more serious attempts at this to succeed.
Incurring context switching for low-level operations is just too slow.
An alternative might be a safe/provable language for kernel and drivers where the compiler can guarantee properties of kernel modules instead of requiring hardware guarantees, and it ends up in one address space/protection boundary. But then the compiler (and its output) becomes a trusted component.