În informatică , o specificație formală este o descriere matematică a unui sistem software sau hardware care poate fi implementat conform acestei descrieri. Specifică ce ar trebui să facă sistemul, nu cum ar trebui să o facă. Dacă există o specificație de sistem, este posibil să se aplice metode formale de verificare pentru a demonstra că sistemul satisface (sau va îndeplini) specificația. Astfel, este posibil să se verifice dacă un anumit model proiectat va satisface cerințele după implementare. Dacă verificarea software examinează conformitatea unui program cu o specificație, atunci validarea examinează conformitatea unui program sau specificație cu cerințele utilizatorului .