SPARK is a formally defined computer programming language based on the Ada programming language, intended for developing high-integrity software used in systems where predictable and highly reliable operation is essential. It facilitates developing applications that demand safety, security, or business integrity. It has especially found use in real-time computing and embedded systems where issues of safety-criticality or computer security are paramount. SPARK is also designed to eliminate all language constructs that can cause unpredictable behavior.

Subsequently the language was progressively extended and refined, first by Program Validation Limited and then by Praxis Critical Systems Limited. In 2004, Praxis Critical Systems Limited changed its name to Praxis High Integrity Systems Limited, and work on SPARK continued.

SPARK has been used in several high-profile safety-critical systems, covering commercial aviation (the Ship/Helicopter Operational Limits Instrumentation System,).

In terms of the approval processes necessary for such systems, SPARK has been used to certify against the UK Defense standard (DEFSTAN) 00-55,

In August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented Skein, one of the SHA-3 candidates, in SPARK. After careful optimization, he managed to have the SPARK version run only about 5 to 10% slower than the C implementation. Later improvements to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.

NVIDIA have also adopted SPARK for the implementation of security-critical firmware. Finding success in this, the company added SPARK for extra firmware-related projects and began in-house training in use of the SPARK technology. The SPARK version of the library has a complete auto-active proof of type-safety, memory-safety and some correctness properties, and retains constant-time algorithms throughout. The SPARK code is also significantly faster than TweetNaCl.