I'm familiar with L4 (and it's various relatives) and I rather like the kernel, although I think it needs a lot of work to achieve anything close to good security. That's not really the kernels fault of course, it's only part of the problem, and there's really very little wrong security wise with the actual kernel, but a kernel by itself is only a very tiny piece of the overall security of the system, it's the other system utilities and even the filesystem itself that's the biggest security problem. Pointing at a kernel and calling it secure as opposed to an OS (and all the baggage that entails) is a little like pointing to a safe and calling it secure as opposed to a bank. It doesn't matter how badass your safe is if anyone can walk in, pick it up, and walk off with it, it's a layered approach to security that makes it secure, and somewhere along the way people need to be involved. Security always comes down to people at some point, and as such anything that does not quantify the person and take them into account is not truly secure. To go back to our previous metaphor of the safe, you can mathematically prove the number of combination's the lock might have, and you can mathematically prove the physical strength of the various components, but what you cannot do is mathematically prove that the guy in charge of guarding that safe is doing his job, or that someone won't somehow manage to steal the safe itself.
Now, formal verification is a nice tool, it lets you efficiently spot certain kinds of problems, but formal verification by itself is far from a good measure of how "secure" something is. A good secure OS must be both free from code defects and exploits (buffer overflows, various injection attacks, escalation bugs), and must be designed with an overall goal of ensuring that the user is given all the tools and information they need in order to make informed judgments about the state of the system.