2016 GPL Edition Now Available!

SPARK GPL 2016 - the formal method verification toolset - includes a number of major enhancements. New language features include in particular support for concurrency with Ravenscar and support of type predicates.

Proof capability has been improved with the integration of a third prover (Z3) in addition to Alt-Ergo and CVC4. A summary of analysis results is now available in a global summary table.

Usability has also been enhanced through the generation of counterexamples for unproved properties, the introduction of predefined proof levels and the definition of user profiles in GPS.

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