How does this compare to the state of the Windows kernel? Serious question.
They use a theorem prover to validate drivers.
Static analysis is a enforced on the Windows source code via the Security Development Lifecycle Checks.
VC++ has quite a few security options that are enabled and used to compile the kernel.
After the whole Windows XP Swiss cheese episodes they ramped up quite a few security processes.
Windows 10 allows for individual application sandboxing.
Not only we have millions of embedded devices shipping microkernel OSes on them, we also have the transition to type-1 hypervisors, and now the slow adoption of unikernels.
Also Apple, Microsoft and Google are increasing the scope of sandboxing on their OSes.
There were some BUILD 2016 presentations about Window 10 sandboxing, but I would need to search for them, which I cannot currently do.