GapFree maakt gebruik van transactionele beweringen die betrekking hebben op het gedrag van het hele circuit, waardoor een grondige dekking wordt gegarandeerd. Een volledigheidscontrole identificeert en verhelpt nauwgezet eventuele hiaten in de verificatie, zodat geen enkel aspect van het ontwerp ongecontroleerd blijft. Het identificeert nauwgezet hiaten in de specificaties en vult deze aan met passende transactionele beweringen, die vervolgens worden geverifieerd aan de hand van het register transfer level (RTL). Alle zwakke beweringen over transacties worden opgespoord, versterkt en vervolgens geverifieerd om de robuustheid en nauwkeurigheid te behouden. Ontbrekende beweringen over transacties worden geïdentificeerd, er worden aanwijzingen gegeven om ze te ontwikkelen en later worden ze grondig geverifieerd aan de hand van de RTL.