Une spécification de premier niveau qui est écrit dans un langage formel mathématique pour permettre des théorèmes montrant la correspondance de la spécification du système à ses exigences formelles à l'hypothèse et formellement prouvé.