industry news
Subscribe Now

New SPARK Adoption Guidance Published

Free booklet, co-authored by Thales, explains how to exploit SPARK/Ada technology to achieve high levels of software assurance


ANNAPOLIS, Md., High Confidence Software and Systems Conference, May 8, 2017 – AdaCore today announced the publication of a free booklet, Implementation Guidance for the Adoption of SPARK, which explains how best to introduce and make use of the SPARK/Ada formal verification technology based on a project’s assurance goals. Co-authored by AdaCore and Thales, a global technology leader in critical domains, the booklet describes the various levels of software assurance at which the SPARK language and toolset can be used. It explains the associated benefits and costs at each level, and details the processes that Thales is using to introduce formal verification in operational projects. The booklet will be a valuable resource for project leaders, technology experts, and software developers responsible for producing high-assurance software for critical systems.


After briefly introducing the Ada language and its SPARK subset, the booklet describes four levels of software assurance:


  1. Stone level – Adhering to the SPARK subset. This is an intermediate step during technology adoption.
  2. Bronze level – Proving proper initialization and correct data flow. This level is recommended for the largest part of the code that is possible and will, among other things, prevent reads of uninitialized variables and misuses of global data.
  3. Silver level – Proving absence of run-time errors. This level is recommended for critical software, for example if it needs to be certified against software standards such as DO-178B and DO-178C (avionics) or EN 50128 (rail).
  4. Gold level – Proving key integrity properties. This level is appropriate for a subset of code where critical safety or security properties need to be shown.


A fifth level, Platinum, entails a full functional proof that the software meets its formally specified requirements. This level is outside the scope of the booklet.


“From our years of providing SPARK solutions to critical industries, we know that it can take time and effort to introduce disruptive technologies into an established workflow, even when the benefits are clear,” said Yannick Moy, SPARK Product Manager at AdaCore. “That’s why I’m pleased that we had the opportunity to work with Thales on this booklet. Now any organization developing and verifying high-assurance software will find practical guidance on how to adopt and best exploit SPARK technology.”


“Introducing formal verification in a project requires an informed scoping of the targeted software functions, as well as a clear definition of the verification objectives,” said Véronique Normand, Research & Technology Manager at Thales. “This booklet is intended to help teams characterize their verification objectives, and to provide practical implementation guidance in applying SPARK. Developed together with several Thales software architects, it is now used to support further SPARK initiatives in the Thales Group.”


About AdaCore

Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings:


  • The GNAT Pro development environment for Ada, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability,
  • The SPARK Pro verification environment, a toolset based on formal methods and oriented toward high-assurance systems,
  • The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software, and
  • The QGen model-based development tool, a qualifiable and customizable code generator and verifier for Simulink® and Stateflow® models, intended for safety-critical control systems.


Over the years, customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as railway systems, space systems, commercial avionics, military systems, air traffic management/control, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see for further information.


AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris.


About Thales

Thales is a global technology leader for the Aerospace, Transport, Defense and Security markets. With 64,000 employees in 56 countries, Thales reported sales of €14.9 billion ($16 billion) in 2016. With over 25,000 engineers and researchers, Thales has a unique capability to design and deploy equipment, systems and services to meet the most complex security requirements. Its exceptional international footprint allows it to work closely with its customers all over the world.


The booklet is available for free, both on-line and as a paper copy; please visit

or contact

Leave a Reply

featured blogs
Feb 20, 2018
It's nearly time for embedded world 2018 (yes, it likes to be trendy and put it all in lower-case), which takes place February 27 to March 1. It happens every year in Nuremberg, and is the biggest embedded conference in the world. Cadence will be there. It is a busy week...
Feb 19, 2018
 56 Gbps PAM4 At DesignCon 2018, Matt Burns (Technical Marketing Manager of Samtec) and Ivan Madrigal (SerDes Systems Application Engineer at Xilinx®), walk us through a combined Xilinx-Samtec 56 Gbps PAM4 backplane demonstration. One port of 56Gbps PAM4 PBRS31 data is...
Feb 19, 2018
Next week, Tuesday-Thursday, is what I believe to be the biggest event dedicated to embedded system development on the planet: Embedded World. It is a massive show. The exhibition includes just about anything remotely connected with embedded design. It is so large that there ...
Jan 19, 2018
Artificial intelligence (AI) is reshaping the way the world works, opening up countless opportunities in commercial and industrial systems. Applications span diverse markets such as autonomous driving, medical diagnostics, home appliances, industrial automation, adaptive webs...