On the topic at large, I think microkernel vs monolithic is not actually the important distinction in kernel design; robustness could improved vastly if the business logic of a kernel were implemented in a memory-safe language instead of C or C++. Register bashing and system setup won't ever be effectively captured by a typesystem (knowing what the semantics of hardware are is the hard problem, and GIGO applies to typesystems as much as anything), but most vulnerabilities are in code that doesn't directly interact with hardware (even if they're in a driver for some obscure hardware, it's generally the syscall-facing side that gets exploited).
I'd like to see more OS development look at non-UNIX designs, rather than trying a million different ways to implementa UNIX-like interface.