Το GapFree χρησιμοποιεί συναλλακτικούς ισχυρισμούς που περιλαμβάνουν ολόκληρη τη συμπεριφορά του κυκλώματος, εξασφαλίζοντας πλήρη κάλυψη. Ένας έλεγχος πληρότητας εντοπίζει αυστηρά και αντιμετωπίζει τυχόν κενά επαλήθευσης, διασφαλίζοντας ότι καμία πτυχή του σχεδιασμού δεν παραμένει ανεξέλεγκτη. Προσδιορίζει σχολαστικά κενά προδιαγραφών και τα κλείνει με κατάλληλους ισχυρισμούς συναλλαγών, οι οποίοι στη συνέχεια επαληθεύονται σε σχέση με το επίπεδο μεταφοράς μητρώου (RTL). Τυχόν αδύναμοι ισχυρισμοί συναλλαγών εντοπίζονται, ενισχύονται και στη συνέχεια επαληθεύονται για να διατηρηθεί η ευρωστία και η ακρίβεια. Ταυτοποιούνται τυχόν ισχυρισμοί συναλλαγών που λείπουν, παρέχονται συμβουλές για την ανάπτυξή τους και αργότερα, επαληθεύονται διεξοδικά έναντι του RTL.