Adesea folosită în testarea circuitelor informatice și a software-ului, verificarea formală este atunci când funcția acestor sisteme este analizată folosind formule matematice. În cazul dezvoltării de software, procesul este de obicei utilizat pentru a arăta dacă programul funcționează corect, pe baza unui model predeterminat. Uneori, modelul teoretic este dovedit a fi nesatisfăcător. În plus față de codul sursă al software-ului, verificarea formală poate fi utilizată în dezvoltarea circuitelor combinaționale, care sunt utilizate pentru a efectua calcule în computere, precum și în memoria computerului. Diferitele abordări includ verificarea ulterioară, verificarea în paralel și verificarea integrată în plus față de diferite metode.
Procedurile matematice pentru calcule, numite algoritmi, sunt utilizate în verificarea formală pentru a testa funcțiile produselor în fiecare etapă de dezvoltare. Dezvoltatorii de software pot găsi erori sau bug-uri atât în codul sursă, cât și în modelul utilizat pentru a-l construi în primul rând. Uneori, modificări fundamentale în modul în care este scris codul pot fi făcute înainte ca o eroare de proiectare să afecteze rezultatul final. Pasul de verificare ajută, în general, la determinarea dacă produsul face ceea ce a fost intenționat să facă și îndeplinește specificațiile aplicației pentru care este.
Verificarea formală poate avea loc atunci când un produs este finalizat, ceea ce se numește verificare ulterioară. O metodă standard, utilizată pe tot parcursul procesului de proiectare și dezvoltare, nu este analizată până când sistemul este terminat. Localizarea erorilor grave în această etapă duce adesea la revizuiri costisitoare și consumatoare de timp. Dezvoltarea și verificarea pot fi efectuate și de două echipe separate pentru verificare în paralel. Prin intercomunicare, dezvoltatorii se pot concentra pe sarcini independente pe parcursul întregului proces de proiectare.
Verificarea integrată este atunci când o echipă realizează dezvoltarea și evaluarea necesară. Conceptele matematice complexe sunt adesea folosite pentru a verifica capacitățile produsului pe parcurs. Metodele de verificare formală variază între proiecte, dar una folosită des este verificarea modelului. Un model hardware sau software constă din diferite proprietăți pe care designerii le doresc în produsul finit. Modelul și sistemul pot fi verificate periodic pentru a vedea dacă proprietățile se potrivesc.
O altă tehnică în verificarea formală implică utilizarea formulelor matematice și a logicii pentru a reprezenta un sistem și proprietățile acestuia. Regulile definite într-un sistem formal se găsesc în general în logică. Ambele tehnici folosesc diverse mijloace pentru a determina dacă o anumită specificație a unui produs este îndeplinită. Dezvoltatorii pot folosi diferite tipuri de software în procesul de verificare formală, fiecare adaptat unui anumit sistem sau limbaj de programare.