SPARK Pro
Replace Testing with Certainty.
SPARK Pro empowers you to write your best code ever. SPARK Pro verifies the safety, security and correctness of your software using formal proof. You will prevent vulnerabilities, eliminate bugs, prove functional correctness, and reduce lifecycle costs for embedded and high-integrity software at scale.
Contact UsSPARK Pro Solves
Security Vulnerabilities
Exploited security vulnerabilities in high-integrity systems are expensive. SPARK prevents vulnerabilities from happening through static memory safety and proven absence of runtime errors.
Undefined Behavior
Many difficult-to-find bugs arise from undefined behavior in software. SPARK ensures safety by eliminating undefined behavior statically, through the SPARK language and mathematical proof.
Broken Reuse
Implicit assumptions make reusing existing software a new context risk. SPARK captures specifications as contracts directly in the code. As your code evolves, SPARK proves the specified requirements remain met.
Untestable Code
Some code is practically untestable, like firmware and very low-level embedded code. SPARK proves functional correctness, replacing testing with guaranteed coverage of all possible inputs across all possible program paths.
What is SPARK?
SPARK is a programming language derived from Ada, designed to eliminate undefined behavior and enable formal verification. It restricts certain language features to guarantee determinism and analyzability, while enriching Ada with precise semantics and annotations that allow developers to prove the absence of defects and verify functional correctness. Writing in SPARK means working in a full-featured, imperative language that compiles directly to the hardware, delivering formally proven, high-performance code you can trust.
SPARK Pro Enables
SPARK Pro combines a programming language and a set of highly automated formal methods into a single product that is demonstrated to work at scale on high-integrity and embedded industrial software.
Absence of Runtime Errors
Run-Time errors includes issues traditionally found by automatic checks at run-time and defensive code, such as out-of-bound array access, division by zero, overflow and more. SPARK proves that no runtime errors are possible in your code. So you can disable these checks at runtime, both eliminating errors and improving runtime performance.
Memory Safety
Through a combination of mitigation of dynamic memory usage, borrow-checking analysis and advanced formal proof, SPARK formally demonstrates absence of memory issues such as use after free, access to uninitialized memory or memory leaks and corruption.
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 Undefined Behaviors
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.
What SPARK Pro Brings
For over 30 years, SPARK has been at the forefront of practical, industrial-strength formal methods. SPARK Pro is the culmination of relentless improvements that span coverage of Ada-language features, user experience, and best-in-class automation. There's never been a better time to get started with deductive formal verification.
Usable
IDE Integration
SPARK Pro is fully integrated into GNAT Studio and Visual Studio Code. So you can get actionable feedback about your code, right from your development environment.
A Single Language
The SPARK language is used for both software implementation and contracts. And the SPARK language scales with you from SPARK Flow to SPARK Proof. So once you learn SPARK, the full power of SPARK Pro is at your disposal.
Rich Feedback
SPARK Pro's error and warning messages are verbose, linked to detailed explanations, and offer suggestions for fixes whenever possible.
Sound
Soundness
SPARK Pro is a sound analysis tool: with SPARK, you don't have to worry about unreported bugs (false negatives).
Precision
SPARK analysis is precise. For some properties, users add annotations that help guide the automation to a successful proof. Typically, this results in proof of all properties - so there are no nuisance messages and few justifications of unproved properties.
Assumptions
SPARK makes carefully designed, useful simplifying assumptions that allow us to maximize scalability and automation. For each assumption, we either check it or document it clearly in the SPARK User’s Guide.
Scalable
Modularity
SPARK Pro analyzes your code one subprogram at a time. So it doesn't experience exponential growth as your software gets bigger.
Parallelism
SPARK Pro will take advantage of as many CPUs as you give it, speeding up analysis. So you get results as quickly as possible.
Automation
SPARK Pro proves absence of runtime errors and functional correctness automatically, integrating best-in-class SMT solvers like cvc5, z3 and alt-ergo. No manual proof required, here.
Industrial
Built for Teams
SPARK Pro is designed to support teams, enabling sharing of analysis results and acceleration for deployment in DevSecOps pipelines.
Target Support
SPARK offers the same supported platforms as GNAT Pro - and the list of supported platforms is growing all the time. And AdaCore is always ready to work with you to add your desired target to the list. So you can be sure you will have the support you need on the target you want.
Professionally Supported
SPARK Pro is backed by AdaCore's best-in-class professional support. If you have an issue using SPARK Pro, we'll unblock you.
Speak to an Expert
Discover the advantages that SPARK Pro can bring to your high-integrity systems.
Get More from SPARK Pro
GNAT Pro
SPARK Pro depends on GNAT Pro for compilation and code generation. Only GNAT Pro is able to compile SPARK programs.
Mentorship
SPARK represents a new programming paradigm. Our mentorship programs ensure your teams are ready to get full value from adopting SPARK Pro.
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.
Hillrom decided to migrate from C++ to Ada and SPARK for ECG algorithm development. This includes both new code as well as translation of some legacy C++ applications to Ada and SPARK.
SPARK has a capability that is not found in most other programming languages. That is the ability to specify program requirements within the code itself and use the associated set of tools to ensure that the implementation matches its requirements. Essentially you are proving your programs are correct. That’s a very powerful capability.
Build High-Integrity Systems You Can Rely On
Build software that proves it’s right.
SPARK Pro helps you eliminate bugs, verify correctness, and ensure safety from the start.
