Most such critical software is written in Ada or C and run on an real time operating system.

A functional programming style or (almost) pure functional language would help to with (semi) automatic static code proofing.