[CHY872]

Are you sure that Ada compilers are verified correct?

I'm pretty sure that the only industrial formally verified compiler is CompCert (for C), though I could be wrong. The motivation for CompCert was certainly that Airbus wanted such a compiler.

Ada wouldn't be a better choice simply because it's designed for security. It'd be a better choice if it turned out better in practice. I've read some of the studies that have been done, and I haven't found them convincing.

Requiring additional tools just isn't a problem, if it works well. Don't criticise the process, criticise the result.