Dimostrazione formale che un vincolo non possa mai essere violato in un dato dominio.
Solitamente, le garanzie hanno un codice di tre lettere, nel formato ABC.
ABC
