The SPARK Programming Language
SPARK, which is based on Ada, offers unparalleled safety and security through its design and support for deductive formal verification. You simply can’t write better code.
Key Advantages of SPARK
Foundations of the Ada Language
SPARK is based on the Ada programming language. All of the benefits of the Ada language translates directly into benefits for SPARK. Wherever you can use Ada, from large server to small devices, you can use SPARK.
Absence of Runtime Errors
Ada helps to ensure software is safe, secure and free of undefined behavior through robust runtime checks that are part of the language. These cover categories like out-of-bounds array accesses, divisions by zero, arithmetic overflow, null dereferences, and more. SPARK proves that these runtime errors will never occur, statically. So you can disable these checks at runtime safely, improving performance.
Memory Safety
SPARK proves memory safety, statically. When access types (pointers) are required, SPARK applies an ownership model that guarantees initialization, non-aliasing, and freedom from memory leaks. So you can be assured your software is memory safe.
Functional Correctness
SPARK proves that user-provided contracts are met by the software implementation. Far beyond testing, these proofs cover all possible combinations of all possible inputs.
No Dynamic Checks or Defensive Code
SPARK proves that defensive code and other run-time checks that may be inserted in the code will never fail. The checks can be removed from the compiled code, ensuring optimal efficiency while retaining guarantees of integrity.
No Undefined Behavior
SPARK is a dialect of Ada that removes Ada features leading to undefined behavior and extends Ada's support for formal specification. When you develop in SPARK, you're using the safest, most secure Ada possible.
Strong Typing
SPARK is a strongly typed language. Building upon Ada, types in SPARK are fundamental elements of the software design. They are named, associated with properties, and checked for consistency statically, via proof. When leveraged, SPARK’s type safety prevents errors that arise when mixing up variables or accidentally converting between type representations.
Modularity
SPARK is fundamentally modular. SPARK performs deductive formal verification one subprogram at a time. Called subprograms are assumed to satisfy their postconditions when their preconditions are met. This ensures that SPARK scales and works well in teams. It also lets you use FFI without sacrificing the ability to prove the correctness of your SPARK code.
Build with Formal Methods
Formal methods represent software semantics using mathematics precisely, allowing analysis of software behaviors prior to runtime. SPARK provides deductive formal verification: subprograms are represented as Hoare triples, and SPARK proves that when the subprogram preconditions are met, subprogram execution ensures the postcondition. SPARK proofs are sound - no false negatives, and precise - no false positives, provided timeout is not reached. Since SPARK operates one subprogram at a time, its analysis is scalable. Moreover, you can focus SPARK on only those parts of your software that are of greatest concern.
Our SPARK Technology
SPARK Pro
SPARK Pro provides the fundamental tooling you need to analyze and prove SPARK programs.
GNAT Pro
Because SPARK is built on Ada, SPARK is compiled with GNAT Pro for Ada. So you have access to a rich set of platforms, featuring IDEs, native and cross compilers, a multi-language build system, multi-language debuggers, and configurable runtime libraries.
CodeSonar for Ada
A comprehensive set of tools that enforce coding standards and analyze code metrics. These capabilities are essential when developing certified SPARK code.
GNAT Dynamic Analysis Suite
Provides unit testing and fuzz testing capabilities, along with a structural coverage analysis tool. And when a property is hard to prove, GNAT Fuzz offers automation to simplify fuzzing the specific subprogram with the sticky property, offering fast and actionable refutation if the property in question is false.
Our SPARK Services
AdaCore’s services help teams adopt SPARK with confidence, offering training, mentorship, and certification support tailored to high-integrity projects.
Certification support
Since SPARK is based on Ada, library & runtime certification and tool qualification are available for DO-178, EN-50128, ISO 26262, ECSS-E-ST-40C / ECSS-Q-ST-80C and IEC 61508.
Mentorship
SPARK represents a new programming paradigm. Our mentorship programs ensure your teams are ready to get full value from adopting SPARK Pro.
SPARK Language Training
AdaCore offers tailored training designed to help your team get up and running with SPARK.
When Failure is not an Option
SPARK is playing an increasingly critical role in the development of safety- and security-critical systems — from advanced defense applications and air-traffic management to firmware in medical and industrial automation domains — because its design enforces the elimination of runtime errors, ensures information-flow integrity, and enables formal proof of functional correctness. It is the only technology available today that enables the deployment of formal methods directly on source code at industrial scale. As the demand for mathematically assured software grows, SPARK continues to expand its relevance across industries that tolerate nothing less than provable correctness.
Expert Guidance
Ready to bring the benefits of formal verification to your project? Our team can help you get started with the right tools, training, and support.
NVIDIA: Adoption of SPARK Ushers in a New Era in Security-Critical Software Development
Learn why NVIDIA made the “heretical” decision to abandon C/C++ and adopt SPARK as its coding language of choice for security-critical software and firmware components.
Trusted by Leading Organizations
Organizations worldwide trust our solutions to meet the highest standards of safety, reliability, and performance.
Find answers to common questions about SPARK
SPARK supports pointers (Ada access types) using an ownership model that was derived from that of Rust. So you can use pointers in your SPARK code, provided you follow SPARK’s ownership rules.
You can raise and handle exceptions in your SPARK code. If you propagate an exception, you have to mention it in an Exceptional_Cases contract, in which you specify what the calling subprogram can count on when handling the exception.
Because SPARK code is Ada, SPARK is supported on all the targets that GNAT supports.
