SPARK
From AdaCommons
http://www.praxis-his.com/sparkada/spark.asp
SPARK is a language designed to support the development of software used in applications where correct operation is vital either for reasons of safety or business integrity.
It is essentially a subset of Ada 95 with the addition of structured comments as annotations that allow programs to be statically checked and proven to be free of runtime errors. The SPARK tools do not produce executable code. The source is checked by the SPARK tools and then passed to any Ada compiler for compilation.
