"There's a serious move towards formal verification rather than random functional testing," he writes. "Government agencies like NASA and some defense organizations are spending more and more on these technologies. They're still a PITA [pain in the ass] for the average programmer, but they're often more effective at testing critical systems."

this part is kinda cool because there's also always been a movement for toward this for opensource/commercial security software, at least for the kernel. Of course, we have no such thing today (as in i doubt anyone here runs such a system in production), but the interest is there.