And no. Ada is an imperative language with an expressive type system (especially compared to other imperative languages). But it doesn't require things like mathematical correctness/completeness. You may be thinking of SPARK which is a subset of Ada that uses contracts and a prover to prove the contracts hold.