Comment by AlotOfReading

2 days ago

A formal proof isn't sufficient on its own for safety-critical applications. You also need to show that your assumptions actually hold in the system and that your proof is the right proof for that system.

I usually tell people that safety-critical processes aren't really about eliminating bugs, that's just a happy side effect. They're about ensuring that the risks for the system are known and reasonably mitigated, with documentation to prove it.