[[procedura|Procedura]] per la dimostrazione formale dell'esistenza di una specifica [[garanzia]] in una data [[funzione]].

Gli esperimenti assumono la denominazione di *esperimento `ABC-XYZ`* dal codice della [[garanzia]] e della [[violazione]] che dimostrano.

Sono solitamente formulati come una competizione tra la [[squadra blu]] e la [[squadra rossa]].