Formal verification doesn't mean shit when a cosmic ray bitflips your program counter.

Safety critical systems need to fail safely, because they will fail. Detecting unexpected execution should halt the system and revert it back to a known state (e.g. cycle power).