Sure, but if you can do something to reduce the number of bugs it seems like you should still do that?

I don’t disagree that in general, reducing the number of bugs is a good goal, but there’s always a limit to how far you go. It’s not like every line is formally proven, for example. Just because you can use a specific technique doesn’t mean that you must.

But also I don’t work directly in these industries and so maybe my impression of this aspect of their processes is incorrect.

I actually think far more of these safety of life standards should require formal proof.

IMNSHO the standards were set so low so that C++ could clamber over the low bar, and it's a happy consequence in some sense that Rust has no trouble clearing it, but the bar should be raised considerably instead. Software crucial to the safe operation of an airliner ought to be proven correct, not just slapped together in any of the general purpose languages, including Rust and then subject to a bit more process than for a web app.

That would explode the costs for marginal safety improvements. I think the same effort spent on better requirement engineering would yield more payoff.

Why do you believe this would "explode the costs" ?

Why would the resulting safety improvements be "marginal" ?

Because proving correctness for complex software is difficult and very few people have relevant experience. So it is both labor intensive and you need to pay high wages. I believe the safety improvements are marginal because of my experience in safety critical development. Almost all the bugs we did not find by testing turned out to be problems with the requirements that led to interoperability issues. Proving the correct implementation of wrong requirements would not have helped.