Because the outside world sees Ethereum as a business, and is confused why the foundation doesn't do all of these things which would make the "product" better.

While the Ethereum Foundation sees Ethereum as an ecosystem, much closer to an open source project, and tries to support people who want to contribute to it.

The answer to your question is, nobody has shown up yet who's willing to put in the massive amount of effort required to write the compiler in a formal language.

The closest we've gotten to that is an implementation of the evm: https://jellopaper.org/

Simplicity has a bunch of Coq proofs actually. And Cardano probably has some formal stuff too, but I am not into proof-of-stake.

you'll still only be as correct as your formal proofs (e.g. using formal proofs isn't a replacement for fuzzing)