This is a component of SPARK 2016.  Those looking for the deductive
program verification platform known as why3 should refer to math/why3
instead.

WWW: http://www.spark-2014.org/