Frama-C allows writing formally verified bug-free C. It is certainly tedious though; you essentially have to write two versions of every function: (1.) the actual C code for the function; (2.) a declarative formal specification of what the function does in ACSL (ANSI C Specification Language), stating all relevant pre-conditions that must be met prior to calling the function, and all relevant post-conditions that hold after the function runs. Then you have to add annotations to computation steps in the function code proving it causes the post-conditions to hold if the pre-conditions hold.
Nevertheless, it is extremely powerful because it can prove the correctness of arbitrary heap manipulation algorithms (lists, trees, graphs). You can formally prove complicated C pointer manipulations are correct that cannot be expressed in 'safe Rust'. There is also the CompCert formally verified C compiler.
I've also studied Ada/Spark's formal verification abilities and C is way ahead here. C is also way ahead of C++ because C has far fewer complicated semantic rules that need to be formalized before they can be analyzed. Even parsing C++ is an enormous task.
In the coming decades as the automation and ease-of-use of formal verification tools improves, I think C may well end up being the best choice for security-critical and correctness-critical systems programming. With current tools it is already ahead of Ada, C++, and Rust.
If it's so tedious, maybe someone can come up with a more unified language that accomplishes the same thing?
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.
There's a lot of interesting stuff out there about the Ariane 5 failure, whose guidance system apparently was in Ada.
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.
We already discussed it here: https://news.ycombinator.com/item?id=20931242 (and probably elsewhere, too).
[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.
SPARK does not allow doubly linked lists:
https://blog.adacore.com/pointer-based-data-structures-in-sp...
For example, singly-linked lists and trees are supported whereas
doubly-linked lists are not.
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:
https://github.com/AdaCore/why3
And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C:
https://github.com/gcc-mirror/gcc/tree/master/gcc/config
Compare with CompCert, the formally verified C compiler:
https://github.com/AbsInt/CompCert
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: