2014 GPL Edition Now Available!

SPARK GPL 2014, supporting SPARK 2014, is the first GPL release of the next generation SPARK toolset.

The main features of the new language and toolset are as follows:
  • Convergence with Ada 2012 Syntax
  • Bigger Language Subset
  • Executable Contracts
  • Hybrid Verification (the ability to mix unit proof with unit test)
  • Formal Container Library
  • Generative Mode for Data Dependencies (the ability to perform data flow analysis without explicit global declarations)
  • Improved IDE feedback in relation to information flow and verification errors

You will find documentation about the SPARK 2014 toolset here:

See in particular the SPARK 2014 Toolset User's Guide to get started. You can also read more about the SPARK 2014 language - including a growing number of tips and tricks here:

AdaCore and Altran are dedicated to developing the finest tools available for software development with SPARK and Ada. The SPARK GPL Edition is the development environment for Free Software development and the GNAT Academic Program for use in Academia. SPARK Pro is for commercial/industrial development.

Download SPARK GPL Edition

View the SPARK Comparison Chart

Learn more about the commercially supported version of SPARK – SPARK Pro

SPARK GPL Community: Projects, tools, and courses created by the SPARK GPL Community

  • Automatic selection of flow analysis mode – the Examiner now supports automatic selection of information flow or data flow analysis on a per subprogram basis.
  • Derived Numeric Types – definition of numeric types has been made easier in GPL 2012 by the introduction of language and tool support for explicitly derived numeric types.
  • SPARKBridge preview for Windows – SPARKBridge, a bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers – is now available as a preview to Windows users, allowing them to trial alternate provers for discharging Verification Conditions.
  • Library Additions – the SPARK library has been augmented with several new packages including: Interfaces, Ada.Characters.Handling, Ada.Text_IO
  • Improvements to Proof Tools - the Simplifier now has enhanced reasoning capabilities for modular types, allowing more proofs to be automatically discharged. In addition, the proof summary output (from the POGS tool) has been improved to make the management of the proof process easier for large projects.
    • The SPARK Language Definition
    • Full SPARK Toolset, including Examiner, Simplifier and Checker
    • Supporting SPARK tools: SPARKSimp, SPARKMake, SPARKFormat and POGS, ViCToR Wrapper, and ZombieScope
    • Tutorial material for SPARK GPL and SPARK Pro are included in the accompanying release of the Tokeneer Discovery package.