[WkndTriathlete]

If those places are relying on software to keep people from getting killed you should assume they are already dead.

The Therac-25 case study (linked elsewhere in these threads) is an excellent study on why fail-safes should be mechanical in nature and based on well-known physical processes that have very few, well-studied states. Software has an effectively uncountable number of states; there is no way to guarantee that a complex software system won't fail at a critical moment due to it being in an unexpected, untested state.

There are ways to model software to prove the absence of certain bad behaviors - TLA+, proof languages, and whatever software was used to validate seL4 come to mind - but they are impractical to use on large systems.