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`.