We are pleased to announce our latest release of SPARK Pro! A product that has been jointly developed alongside our partner Altran and following the global AdaCore Tech Days, you can now see the SPARK 2014 talk, Formal Verification Made Easy by AdaCore’s Hristian Kirtchev, on YouTube.

SPARK 2014 has formed the basis for a number of make with Ada projects, from Formal proof on my wrist, which created Tetris in SPARK on the ARM cortex M4, to a project to rewrite the software of the Crazyflie 2.0 in Ada and SPARK to help prevent drone crashes.

SPARK is based on Ada 2012 and aims to provide software verification using formal methods, in order to prove as much as possible and minimise the amount of testing, or altogether eliminate that need if possible. The high level programming language works especially well in a safety critical context, having achieved the avionics standards DO-178C and DO-333.

The SPARK Pro 16.0 integrated development and verification environment uses a mathematics based analysis technology and provides enhanced coverage of the SPARK 2014 language features. Helping to reduce the certification effort for safety-critical and high-security systems.

Check out the video below to understand what it is, the various applications and how to get started today!