(1) Een softwaretool dat als invoer accepteert een computerprogramma en een vertegenwoordiging van de specificatie en produceert, eventueel met menselijke hulp, een bewijs of het practicumverslag van de juistheid van de program.~(2) een softwaretool dat deel automatiseert of alle van het verificatieproces.