Defense contractors and other high-critical systems (think airplanes, space shuttles, missile command) would gladly pay for and accept that level of complexity.

You're generally right about complex specification and verification being popular in the defense and aerospace industries. However, I think that you may be mistaking a secure microkernel for a real-time one.

There are hard real-time variants of L4 out there, but unless that was a primary goal of the NICTA team, I don't think you're likely to see many copies of that kernel running a ballistic missile's avionics package.

A verified secure OS kernel like this would more likely be used as a substrate for building secure servers and workstations, network routers, or mobile communications devices.

I don't think mncaudill was confusing a secure microkernel with a realtime one. Rather, I think he was (correctly) thinking in terms of the reliability requirements those industries have.