Defense contractors and other high-critical systems (think airplanes, space shuttles, missile command) would gladly pay for and accept that level of complexity.
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.