SPARK is a formally defined computer programming language based on the Ada 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.