I'm copying below the announcement for the GNAT GPL 2016 and SPARK GPL 2016 releases, which gives some details about the new features since last year.
Dear GNAT and SPARK GPL user,
We are pleased to announce the availability of the GNAT and SPARK GPL 2016 toolsets.
GNAT GPL 2016 incorporates upgraded technology for the debugger (GDB 7.10) along with support for the Windows 10 platform and many new features.
Ada runtime support has been extended for the STM32f429-disco, STM32f469-disco and STM32F7-disco development boards based on the STM32 family of microcontrollers.
* ravenscar sfp/full for the stm32f429-disco board
* ravenscar sfp/full for the stm32f469-disco board
* ravenscar sfp/full for the stm32f7-disco board
SPARK GPL 2016 - the formal method verification toolset - includes the following new features:
- Support for concurrency with Ravenscar and type predicates
- Generation of counterexamples for unproved checks
- Better support of bitwise (modular) operations in proof
- Generation of global summary table
You will find documentation about the GNAT GPL 2016 and SPARK GPL 2016 toolset here: