Reliability with Formally Proven SPARK Ada

Ada and its subset SPARK is a language initially inspired by Pascal, embedding capabilities to describe specification, implementation and verification all in one platform. This unique integration allows identification and correction of defects early in the development cycles, reducing effort during late phases of development and mitigating risks of errors found after deployment. It can be used from large server environments running dozens of cores on gigabytes of memory down to bare metal small 8 bits microcontrollers below one megabyte, across architectures as diverse as x86, ARM, PowerPC or RISC-V.

Example of Ada Syntax function GCD(N1, N2 : Natural) return Natural is
-- Greatest Common Divisor of two non-negative integers
begin
   if N2=0 then
      return N1;
   else
      return GCD(N2, N1 mod N2);
   end if;
end GCD;

The Ada programming language and its SPARK subset are emerging as compelling alternatives to C for many industries.

Generates Code that is Formally Verified to be Free of Vulnerabilities

The Ada programming language and its SPARK subset combined with its toolset is a platform that allows developers to formally guarantee properties of source code, such as the 100% absence of certain categories of vulnerabilities (buffer overflow, division by zero, references to uninitialized variables, memory corruption), and to prove custom functional assertions.

Increases Critical Code Performance

SPARK and Ada provide performance levels and footprints similar to other system-level languages such as C. However, SPARK allows the removal of proven checks from the final binary, reducing the need for defensive code and allowing for safer and more efficient code execution.

Reduces Development Costs

The demand for cost-effective tools and methodologies has greatly increased in the automotive and industrial domains over the past few years. Using Ada and SPARK reduces the cost of developing safety and security-critical software by automating many verifications that would otherwise need to be done through manual code reviews or testing. It also allows the detection of potential issues early in the development process, reducing the amount of errors needing to be fixed in later stages. For industries that have strong safety, reliability, and security standards, like aerospace and automotive, these benefits can translate to nearly 40 percent cost and time savings from enhanced software verification, according to a study by VDC Research.

Vdc Research Chart

SPARK Technical Testimonies and Use Cases

Large Open-Source Community

Ada is an open ISO standard driven by the Ada Rapporteur Group (ARG). GNAT is a free compiler for Ada that is part of the GNU Compiler Collection (GCC).

The Ada community is passionate about building dependable, high-integrity software. There are a number of resources available to academics, free software developers, or people who just want to learn more about Ada and would like to dive in right away.

Social chat

The Ada/SPARK community is active on several platforms, such as Reddit, GitHub, Twitter, Telegram, and Gitter (Ada chat/Alire chat)

ALR Logo

Open source Ada/SPARK projects are available in the Alire package manager ecosystem

Learn Logo

An interactive learning platform designed to teach the Ada and SPARK programming languages is available at learn.adacore.com

GAP Logo lovelace blue


The GNAT Academic Program (GAP) links teachers of Ada and SPARK the world over

Ada Core U

Several university-level course videos are available on YouTube, and base material, including slides, are available on GitHub

Contact us about your industrial application

AdaCore is specialized in accompanying teams and projects with their evaluation or adoption of the Ada programming language as well as its formally provable subset SPARK. Fill out the form below to request a call with us.