I'm copying below the announcement for the SPARK Discovery GPL 2017 releases, which gives some details about the new features since last year. For the complete announcement about GNAT GPL 2017 and SPARK Discovery GPL 2017, see AdaCore' blog.
For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK Discovery GPL.
SPARK Discovery GPL 2017 offers improved automation of proofs, thanks to improvements in the underlying prover Alt-Ergo and a finer-grain splitting of conjunctions. Interaction during proof has been improved thanks to the new statistics, display and replay modes. Type invariants from Ada are now also supported in SPARK. Note that the optional provers CVC4 and Z3 are no longer distributed with SPARK Discovery GPL 2017 (see the differences between SPARK Pro and SPARK Discovery here), and should be installed separately.
The GPL 2017 release can be downloaded: