But you do know the specification, or at least parts of it in many cases.

In the upstream example, one specification is that some reasonable time after you turn on the airplane, the flight controller is ready to fly. That's a very reasonable spec and important to verify in the given story. It is a thin end of the wedge for a lot of real-time guarantees that you might like to make.

As another instance where the specification is known, what is the specification of compiled object code? The specification of compiled code is the source code and proving that the object code matches the source code is a way to protect against adversarial tool chains. Check out seL4 for an example of this kind of formal verification.

Memory safety is another property susceptible to formal verification. The Rust community is making use of this very nicely.

The net lesson is that even if it is impossible to get formal specifications for lots of things, there are lots of other things where you can define good specifications (and you might be able to prove you meet them, too!).