You might be thinking of type predicates, added in Ada2012 : http://sworthodoxy.blogspot.fr/2015/08/ada-2012-type-invaria... some of them statically provable in Spark : http://www.spark-2014.org/entries/detail/spark-2014-rational... (if interested, there's a link down there with a 'rationale' pdf).