Formální verifikace je způsob, jak u softwaru dokázat správnost místo toho, aby se jen spoléhal na testy. Program se nejdřív popíše formální specifikací — přesným matematickým zadáním, co má dělat — a pak se strojově ověřeným důkazem potvrdí, že kód specifikaci skutečně splňuje, typicky s pomocí nástrojů jako Lean, Coq nebo Dafny. Používá se hlavně tam, kde je chyba drahá: kryptografické protokoly, letový software nebo distribuované systémy.
