The first thing about L4.verified is that formal verification, while admirable, doesn't really matter, at least not in a world where exploits are commodities, exploitation a continuous process: if a program is only a few thousand lines long and written with attention to security, the number of vulnerabilities can at worst be counted on one hand, and attackers will find them all for you in short order. If you're Iran and have an attacker capable of pouring millions of dollars into a single hack, it might make a difference; if you're Microsoft, not so much.

The second thing is that while a microkernel (if used with an IOMMU to prevent a malicious driver from DMAing all over your code) appealingly prevents an attacker from exploiting a malloc overflow in some random network driver and immediately gaining full access to anything (the current state of kernel security!-- but performance is key), it doesn't prevent an attacker from using that network driver pwn to hijack the user's Facebook session; full access is appealing, but in a complex system there are many, many "lesser targets" that are just as bad from a user's point of view.

Microkernels and their little cousin sandboxing can help, but the resulting trusted computing base is still much, much larger than we can formally verify in the foreseeable future.

(A sibling of this comment mentioned Singularity, but that's a fairly different beast: instead of proving that fast code is safe, you try to make obviously (memory) safe code fast. The only reason Singularity is able to make interesting performance claims is that it uses verification to completely avoid system calls: pretty cool, but a NaCl-like kernel could do something fairly similar for C; it doesn't really change the correctness/performance tradeoff.)