(1) Softvérový nástroj, ktorý akceptuje ako vstup, počítačový program a reprezentácia jeho špecifikácii a produkuje, prípadne s ľudskú Pomocníka, dôkaz alebo vyvrátenie správnosti program.~(2) akékoľvek softvérový nástroj, ktorý automatizuje časti alebo celého procesu overovania.