Disappointing to see such a long article and no mention of type theory, or any other work from the "correct by construction" school of formal methods. It's all normie model checking, TLA+ etc.
Formal methods can ensure that the code matches a formally written spec, for all the aspects of the code that are covered by the formal method. Note well: That's not all aspects of the code. And you have the little problem of (correctly) creating the formal spec. This move the problem up a layer, but the problem doesn't go away.
Even given a formal spec, though, it's my impression that formal methods are s l o w. Does anyone have data on this?
How on Earth did we end up putting people who can't write down precisely what they want in charge of programming machines that do exactly what you tell them to?
Huh? Types (of the sufficiently advanced kind) are one way of specifying behavior in the same sense as TLA+ and other models. The difference is that type theory provides a coherent story for how to form entire systems like this in a composable manner. Traditional modeling/spec languages, not so much.