Formalus programos teisingumo patikrinimas įrodant, kad programa yra teisinga.

Programa laikoma teisinga, jeigu ji daro tai, ko reikia, kas apibrėžta jos specifikacijoje. Tam, kad būtų galima formaliai (kompiuteriu) patikrinti programos teisingumą, reikia, kad ir jos specifikacija būtų formali. Parašyti formalią specifikaciją yra sudėtingas uždavinys. Verifikavimo programos taip pat sudėtingos. Todėl verifikuojamos tik labai atsakingos programos.

Programos taip pat tikrinamos testavimu. Testuoti paprasčiau. Tačiau testavimu tik randamos klaidos, bet neįrodoma, kad jų nėra. Verifikavimu įrodoma, kad klaidų nebėra.

Plg. testavimas.