The SPARK programming language allows development of software with automatically generated proofs that they don't contain any run-time errors, and that the properties described in the source text always will be fulfilled.
I have published a few examples of SPARK 2014 source text:
Please call or write if you are interested in development of SPARK 2014 software.
If you have questions or requests, please send them to
<email@example.com>, or call +45 21 49 08 04.