We have Ada/SPARK already. SPARK is a subset of Ada that allows you to formally verify your code, e.g. to prove the absence of runtime errors, memory leaks, and so forth.
Not too interesting; they disabled the checks[1]. Lot of stuff have happened since then to Ada and SPARK. The Ada they used is quite different to the Ada we have today. SPARK 2014 is a complete re-design of the language, too. Plus, you are responding to a comment specifically talking about Ada/SPARK (SPARK specifically), so not sure how Ariane 5 is relevant.
[1] Today those checks may not even be needed to begin with due to SPARK. GNATprove may have given them "predicate check might fail" or something like that. Read the AdaCore Blog for more.
I've used SPARK with GNAT Studio, I've used Frama-C, and I'm also experimenting with CBMC. Frama-C is way more powerful than SPARK, but also consequently has a much deeper learning curve.
For example, singly-linked lists and trees are supported whereas
doubly-linked lists are not.
With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK.
However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.
AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:
Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:
