SPARK Ada is the main competitor & has been in industrial use a long time:

http://www.spark-2014.org/uploads/itp_2014_r610.pdf

http://www.anthonyhall.org/c_by_c_secure_system.pdf

http://libre.adacore.com/tools/spark-gpl-edition/