SPARK

An annotated subset of Ada supported by tools supplied by Praxis Critical Systems (originally by PVL).

http://sparkada.com.