If you’re in the game of producing secure and high integrity software, SPARK just might be what you’re looking for, and with the newly released SPARK GPL 2011 Edition it’s simple to try your hands at SPARK.
At the libre.adacore.com website, there’s a few community created SPARK projects available. These might be worth checking out for some examples on how to use SPARK. Another option is the AdaCore05 YouTube channel, where there are quite a few SPARK related videos to enjoy.
SPARK is developed by altran praxis.