Embedded.com: “You Think Your Software Works? Prove It!” – Describes the use of formal methods with ADA SPARK.