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

WWW: https://forge.open-do.org/projects/spark2014