 Formal verification methods grant an a-priori analysis of the behaviors of programs, without requiring the observation of any of their implementation or considering their execution. In particular, theorem proving allows one to deduce any potential behavior of the program under consideration and its behavioral properties from a suitable axiomatic representation. In the case of model checking, one knows in advance the behavioural properties displayed by the execution of a program by performing an algorithmic search of the formulas valid in a given set-theoretic model. These considerations famously led Hoare (1969) to conclude that program development is an “exact science”, which should be characterized by mathematical proofs of correctness, epistemologically on a par with standard proofs in mathematical practice.