It's possible to prove the correctness of non-functional code too. It also tends to be much easier to reason about the time and space behavior of code written in, say, C. In a system with hard real time requirements that's very important.

You also have to consider the compiler. Proving that your Haskell code is correct is largely pointless if you then compile it with a compiler that hasn't been proven correct. At a minimum that's going to mean compiling the code with a lot of the fancier optimizations turned off, which can lead to a rather severe degradation in performance in the case of a pure functional language.

My guess is that there are not currently any functional languages that (i) are significantly easier to formally verify than C or Ada, (ii) have predictable time and space behavior, and (iii) have implementations that are both extremely well-verified and reasonably performant.

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.