NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities" in which they single out five approaches which have the potential for creating software with 100 times fewer vulnerabilities than we do today. One of these approaches is formal methods. In the introduction of the document, the authors explain that they selected the five approaches that meet the following three criteria:

• Dramatic impact,
• 3 to 7-year time frame and
• Technical activities.

The dramatic impact criteria is where they aim at "reducing vulnerabilities by two orders of magnitude". The 3 to 7-year time frame was meant to select "existing techniques that have not reached their full potential for impact". The technical criteria narrowed the selection to the technical area.

Among formal methods, the report highlights strong suits of SPARK, such as "Sound Static Program Analysis" (the raison d'être of SPARK), "Assertions, Pre- and Postconditions, Invariants, Aspects and Contracts" (all of which are available in SPARK), and "Correct-by-Construction". The report also cites SPARK projects Tokeneer and iFACTS as example of mature uses of formal methods.

Another of the five approaches selected by NIST to dramatically reduce software vulnerabilities is what they call "Additive Software Analysis Techniques", where results of analysis techniques are combined. This has been on our radar since 2010 when we first planned an integration between our static analysis tool CodePeer and our formal verification toolset SPARK. We have finally achieved a first step in the integration of the two tools in SPARK 17, by using CodePeer as a first level of proof tool inside SPARK Pro.

Paul Black who lead the work on this report was interviewed a few months ago, and he talks specifically about formal methods at 7:30 in the podcast. His host Kevin Greene from US Homeland Security mentions that "There has been a lot of talk especially in the federal community about formal methods." To which Paul Black answers later that "We do have to get a little more serious about formal methods."

NIST is not the only ones to support the use of SPARK. Editor Bill Wong from Electronic Design has included SPARK in his "2016 Gifts for the Techie", saying:

It is always nice to give something that is good for you, so here is my suggestion (and it’s a cheap one): Learn SPARK. Yes, I mean that Ada programming language subset.

For those who'd like to follow NIST or Bill Wong's advice, here is where you should start:

• The free SPARK Course on AdaCore U e-learning website
• The online SPARK User's Guide