This is a component of SPARK 2015: Those looking for the automatic theorem prover known as Alt-Ergo should refer to math/alt-ergo instead WWW: https://forge.open-do.org/projects/spark2014