I mean, I think this really depends on how you define ethereum. I think we all agree that there hasn’t been an effective attack against the consensus mechanism in a while (we could argue the original dao was sort of a successful attack against all of eth due to the hard fork).
This is kinda where I’ve gotten to on this: consensus is pretty much safe. Smart contracting is very hard to do safely.
This is not unlike the guarantees in general computation. The metal is pretty safe. The further you get away from the metal, the more layers of abstraction you’re relying on functioning predictably.
To be clear, I’m not arguing with you and appreciate your point about formal verification of eth.