SPARK 2014 comprises a subset of Ada 2012, excluding those features not amenable to sound static verification. SPARK 2014 uses the contract-based programming provided by the latest Ada 2012 version, and uses the Ada 2012 aspect notation to strengthen the specification capabilities of Ada by the addition of new contracts for data dependencies, information flows, state abstraction, and data and behavior refinement.

Once the functional behavior or low-level requirements of a program have been captured as SPARK 2014 contracts, the verification tool-set can be applied to prove that the implementation is correct and free from run-time exceptions automatically. Only where verification cannot be completed by themselves is it necessary to write unit tests, with the same contracts used to check the correct run-time behavior of the relevant subprograms.