SPARK is more than 20 years old at that point and allows you to easily use formally proven code next to other ADA code. Sorry but implying that the issue is things “lost in translation” is a complete cope out.
I’m very sour about the disdain for formal proof in the field. I understand the wish to iterate fast for user-facing elements but the fact that we use the same development techniques for the backbone of our infrastructure is nothing short of insane from my point of view.
There is a self defeating attitude with regard to formal tool which is that they are too costly and too complicated to use outside of things for which they are mandatory. It means people are not trained in how to use them so it’s hard and costly to find someone who will prove your code and this vicious cycle somehow feeds itself.