Airplane code certainly is put through “formal verification”, but also “putting it through formal verification” is not a magic spell that removes bugs from a program. It only proves it does what is in the spec.
It seems like the word “formal” impresses people too much.
Usually, it only proves that a simplified version of the code satisfies to some extent a translation of the spec to some formal language. And "prove" only means that some rather buggy tool printed "Valid".
Every point in this chain can and often does introduces bugs.
However, this does find real bugs in the code, and formalizing code and specs require people to think deeply and formally on aspects of the problem.
It just doesn't prove the code to be correct, or even that it satisfies the actual spec.
It seems like the word “formal” impresses people too much.