SPARK is a programming language, a formally defined sub-set of Ada based on Ada83 and Ada95. It is developed by Praxis Critical Systems (PCS), a UK software developer. PCS claims it was designed for development of software for applications where "correct operation is vital either for reasons of safety or business integrity."
