>critical software goes under a much more rigorous testing regime

Testing is not only not enough, it's also not required :) (as Dijkstra said, it can only show the presence of bugs, not their absence)

For example, the software for some automated subways in France has never been tested, only proven correct (source: https://www.youtube.com/watch?v=jc9QmqKIUj4&t=54m50s).

Similar formal methods are used for critical software pieces in Airbus aircrafts (source: the same speaker as for the linked video, but I don't remember which talk that was in).