Formal verification is great, but cosmic rays don't read our specs.

They do if they’re in the specs. See near-universal use of lockstep processors, ECC etc in safety-critical and high radiation cases, which comes from the two requirements that “a single bit flip from a cosmic ray shall be detectable” and “multiple simultaneous hit flips from cosmic rays shall be shown to be sufficiently rare in the operating environment.”