Implementation Guidance for the Adoption of SPARK

This booklet presents a set of guidelines for adopting formal verification in existing projects, codebases and processes. These guidelines are based on five levels of software assurance, in increasing order of benefits and costs. The guidelines were developed jointly by AdaCore and Thales for the adoption of the SPARK language technology at Thales. They do not require a background in mathematical logic or any specialized expertise, and they allow an evolutionary approach to introducing formal methods into an enterprise.

SPARK has a long and successful track record for high-assurance systems. This booklet shows how to exploit its benefits, and understand its costs, on the path to zero-defect software.

Release 1.2