Part_01 of my comment that is split up due to the 2-links-per-post limitation.
What regards to formal verification, then the main author of the Pentagon programming language, Ada, Tucker Taft, has created a brand new systems programming language,
Part_02 of my comment that is split up due to the 2-links-per-post limitation.
ParaSail (parasail-lang.org), which has the following features:
Formal verification tools come with the compiler. Newest version of the compiler uses the LLVM.
The maximum value of the Integer type is limited only with RAM size.
Totally new threading model: auto-parallelization is part of the language semantics and implementation, id est the same code that can take advantage of 2 CPUs, can take advantage of 1024-CPUs.
No legacy dragged along. The project started as a hobby project of the Tucker Taft and everything is developed mainly by him and really FOR QUALITY, NOT DEADLINES. ParaSail is meant to be the language that is used in the future avionics, nuclear reactors, medical equipment, all other safety-critical systems that benefit from a system programming language.
Part_03 of my comment that is split up due to the 2-links-per-post limitation.
I am NOT a ParaSail developer. I do NOT have any formal association with ParaSail's original author, Tucker Taft. I'm just a fan of his work, who has re-packaged his work (with his help at his ParaSail forum). My version differs from Tucker Taft's (id est the upstream) version mainly by the fact that my version is tailored for servers and robots, while the Tucker Taft's version builds/compiles only, when GUI-libraries are available. (He told me at his ParaSail forum, how to outcomment the GUI library dependencies.)
(Due to the 3 posts per thread limit for new users my comment continues at my site.)