Using Ada Contracts
Ada 2012 introduced the idea of contracts. This TechXchange includes articles that delve into how they work and why contracts are useful. Contracts are also the basis for SPARK, a version of Ada that allows a program to be proven statically based on the contracts defined with a program.
More Articles About Ada/SPARK Contracts and Formal Verification
More Resources on Ada/SPARK Contracts and Formal Verification
Here are some useful links on this topic.