One possible reason to choose SPARK over other solutions is the benefits that it brings in a certification context, for reaching some of the verification objectives. For example, the previous version of SPARK has been used both in a safety certification context and in a security certification context. With SPARK 2014, we target in particular the avionics domain, whose recently updated certification standard DO-178C accepts the use of formal verification as justification for many verification objectives.

While certification authorities in railway have long recognized the use of formal methods, and a few companies like Airbus and Rockwell Collins have pioneered the use of formal methods in avionics, we still are at the beginning of the adoption of formal methods in industries submitted to certification constraints. Which means that many people simply don't know yet how they should present the use of formal methods to the certification authorities to obtain the credit they expect from it.

This was the reason that pushed in 2010 for the creation of the workshop on Theorem Proving in Certification. Since then, the group has had 3 gatherings in Oxford, the last of which in December last year, during which we decided to work on a shared document gathering recommandations for the use of formal methods in certification. This draft document is now publicly available here:

https://docs.google.com/document/d/1nTXzxHLXg9s97mxtrEOS8rfgUNGK3dnW7L43WwU7Lpo

If you're interested in this topic, don't hesitate to send comments about the above document to the public mailing-list tpcert@googlegroups.com. You can also participate more actively in the discussions by joining the googlegroup.