GapFree uporablja transakcijske trditve, ki zajemajo celotno vedenje vezja in zagotavljajo temeljito pokritost. Preverjevalnik popolnosti natančno identificira in odpravi morebitne vrzeli pri preverjanju ter zagotavlja, da noben vidik zasnove ne ostane nepreverjen. Natančno prepozna vrzeli v specifikacijah in jih zapre z ustreznimi transakcijskimi trditvami, ki se nato preverjajo glede na raven prenosa registra (RTL). Vse šibke transakcijske trditve so natančno določene, okrepljene in naknadno preverjene, da se ohrani robustnost in natančnost. Ugotovljene so vse manjkajoče transakcijske trditve, podani so namigi za njihovo razvoj in kasneje temeljito preverjeni glede na RTL.