Verifikasjon (informatikk)

I informatikk og programvareteknikk forstår man med formell verifikasjon det matematiske bevis som kan vise at et implementert program oppfyller en gitt spesifikasjon. Slike bevis blir utført ved hjelp av metoder for formal semantikk. At verifikasjon ikke er mulig i alle tilfeller, er påvist teoretisk ved f.eks. Turings stopproblem og Gödels ufullstendighetsteorem.