You are forgetting nondeterministic aspects. Only in theory, aircraft and atmosphere is a deterministic Newtonian machine, in practice, less so. But even if so, physics simulations can't be done and evaluated for all possible initial conditions for even the simplest model.

One can imagine a mental model of airplane and make a formal design for it. Then do a formal check in the most important scenarios that introduce weather, human action, system failures. The design will always fail for some scenarios. Not a problem if those are not important (in terms of risk). But which scenarios are the important ones? Probability and severity of consequences of those scenarios are much needed knowledge, and one can find those only via the good old method of iterative testing in wild.

But it obeys the laws of physics perfectly as it nosedives into the ground.

It also has a user interface. Are you saying it's possible to formally quantify human behaviour as well?

Every program has a inputs, and with that some more ore less direct version of a user interface. You define the acceptable input values and then define what happens with unacceptable ones (and same for combinations).

If that were not verifiable, then no program would be.