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.