SPARK Pro (original) (raw)

SPARK Pro Created with Sketch.

Industrial-Strength Formal Methods.

SPARK Pro is ready to deliver unprecedented and unsurpassed security, correctness and safety for industrial-scale embedded and native applications.

No other language, tool, or methodology can compete at this scale. You simply can’t write better code.

Learn more about SPARK Speak to an expert

Customer Projects: SPARK Pro

Security. Built In.

The SPARK language - drawing on its roots in Ada - and SPARK analyses - SPARK Flow and SPARK Proof - work together to make your code secure.

SPARK Pro prevents or detects important classes of security bugs - including those that lead to many of the top 10 weaknesses cataloged in the CWEs. Unlike most languages, in which making mistakes that lead to security bugs is too easy, the SPARK language provides memory safety out of the box - including freedom from buffer overruns. SPARK Proof extends this core memory safety to include freedom from memory leaks.

Safety. From the Ground Up.

The SPARK language and SPARK analyses work together to

make your code safer.

SPARK Pro starts with a firm foundation - the SPARK language - to provide safety. Unlike most programming tools, in which misusing features like pointers, dynamic memory allocation, and user-raised exceptions is too easy, SPARK Flow and SPARK Proof prove that code recovers from exceptions correctly, is free from runtime errors, and uses pointers and dynamic memory correctly. So you can be certain that your code will work correctly in its initial application and can confidently reuse your code in new applications.

Better Software. Lower Cost.

The SPARK language and SPARK analyses work together to prevent or detect many kinds of bugs automatically - before you even build and test your software.

SPARK Pro guarantees that many classes of bugs are prevented or detected during software development. And you can take this assurance even further by writing your specifications as contracts and proving that your code satisfies them. The result is software with an exceptionally low defect density. Since bugs introduced during software development are exponentially more expensive to fix in later phases - like integration testing, acceptance testing, or deployment - you save time and money over the lifetime of your application.

Discuss your requirements with a technical expert

Verification. Without Testing.

SPARK Proof provides formal verification that is automatic, reproducible, and integrated into the software development process. In many software applications - especially low-level, embedded applications like firmware - testing is impractical or impossible for some parts of the code. But once you've used the SPARK language to capture your specifications as contracts, SPARK Proof will prove that your code satisfies its contract. So you can be sure your software is correct, even when testing is impossible. Even while your software is changing.

SPARK Pro streamlines verification activities.

Future Proof.

The SPARK language allows you to capture your specifications as contracts so that you can prove that your code satisfies them. Unlike most programming languages, for which specifications must be written in natural language and are disconnected from the code, when your SPARK specifications change, you'll know immediately where you need to update your SPARK code. And as you change your code - for example, to optimize your algorithms - you can be sure the changes still satisfy the contracts. So you never have to worry about your specifications and your code getting out of sync.

SPARK Pro prevents the drift between specification and code.

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.

Ready to get started with SPARK? Talk to a technical expert

Easy to Use.

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. You can learn more about the SPARK language in the Intro to SPARK course at learn.adacore.com.

SPARK Pro's error and warning messages are verbose, linked to detailed explanations, and offer suggestions for fixes whenever possible. Moreover, SPARK is fully integrated into GNAT Studio and VS Code. So you can get actionable feedback about your code, right from your development environment.

It’s never been easier to get started using formal methods.

Easy to Adopt.

The SPARK language is designed to offer safety and security out of the box. So you could adopt SPARK Pro and stop at just using the SPARK language. But we think you’ll want to go further, to get the most out of SPARK Pro as possible.

SPARK Flow offers additional guarantees on top of the SPARK language at no additional cost, reporting problems with data initialization or use. You can take SPARK Flow further by describing your intended data and information flows; SPARK Flow will tell you if your implementation matches your intent.

SPARK Proof takes the guarantees further, but does require more effort. Using the SPARK language, you describe your software’s intent through the provision of contracts. Depending on the complexity of your contracts and software, you may have to use the SPARK language to describe how your software works towards the fulfillment of the contract.

Writing code that proves in SPARK is harder than just writing code. Just like writing code in a statically-typed language is harder than writing code in a dynamically-typed language. That’s why SPARK Pro offers the incremental approach to adoption described above - so you can decide how far you want to push your adoption of SPARK Pro on a unit-by-unit basis.

No matter what you decide, SPARK will be there every step of the way.

Easy to Scale.

SPARK Pro is sound, precise, and modular. So it doesn't experience exponential growth as software gets bigger. SPARK is ready to run on developer machines as well as in DevSecOps pipelines and supports rapid analysis by sharing proof state across instances. So SPARK is ready to scale from small programs to full-size industrial applications - all with the same ease of use.

Relevant Analyses.

SPARK Flow and SPARK Proof analyze the SPARK language directly - without relying on simplifying abstractions that introduce semantic differences between the code and the proof.

The semantics of SPARK contracts are the same as the semantics of the SPARK language, unlike many formal methods that interpret the semantics of the code differently from the actual operational semantics of the code. Integers are machine integers with upper and lower bounds. Arrays are Ada arrays. Floats are IEEE floating-point numbers. And operators - like equality - may be overridden with user-provided semantics. SPARK is aware of and reasons about all of these details and more. So you can be sure that the proof results are really relevant to the code that will execute on your target. You can even retain your contracts and execute them at runtime. You've never had this much assurance that your software is correct.

Expert Support

SPARK Pro is provided with AdaCore’s best-in-class support: when we provide support, we put you in touch with the experts - the engineers who develop and maintain the product. Our support is a critical part of our business model and something we take very seriously.

Learn more about Expert Support

Learn more about SPARK

Explore Our Engaging Webinar Series on SPARK Pro