Writing very reliable software

Here's an article in IEEE Spectrum about Praxis, a British firm specializing in extremely high reliablity software. The interesting features about their development approach are that they spend a lot of time up-front writing a requirements specification, implementing the software first in Z, a formal predicate languange so the code can be mathematically proven correct, and finally doing the actual coding in Sparks, a language derived from Ada. Ada, in turn was designed from the start to write reliable code.