> Relative to what?

Relative to C++.

> There are formal verification tools for other languages.

None that are actually used.

I have no horse in this race and I have never actually written any Ada, but it seems pretty clear to me that it would produce more correct code on average.

Looking at the Ariane 5 error it looks like the specifically disabled the compile-time error: https://www.sarahandrobin.com/ingo/swr/ariane5.html

That's nothing to do with Ada.

Also asking for evidence is a red herring. Where's the evidence that Rust code is more likely to be correct than Perl? There isn't any. It's too difficult to collect that evidence. Yet it's obviously true.

Plenty of things are pretty obviously true but collecting scientific evidence of them is completely infeasible. Are code comments helpful at all? No evidence. Are regexes error-prone and hard to read? No evidence. Are autoformatters helpful? No evidence.