Formální ověření nebo formální důkaz je formální důkaz shody nebo nesouladu předmětu ověřování s jeho formálním popisem. Předmětem jsou algoritmy, programy a další důkazy.
Vzhledem k rutinnosti i jednoduché formální verifikace a teoretické možnosti jejich úplné automatizace, formální verifikace obvykle znamená automatickou verifikace pomocí programu .
Testování softwaru nemůže prokázat, že systém, algoritmus nebo program neobsahuje žádné chyby a defekty a splňuje určitou vlastnost. To lze provést formálním ověřením.
Formální verifikaci lze použít k ověření systémů, jako je software zdrojového kódu, kryptografické protokoly , kombinatorické logické obvody , digitální obvody s vnitřní pamětí.
Verifikace je formálním důkazem na abstraktním matematickém modelu systému za předpokladu, že korespondence mezi matematickým modelem a povahou systému je považována za původně danou. Například k sestavení modelu nebo matematické analýzy a důkazu správnosti algoritmů a programů.
Příklady matematických objektů často používaných pro modelování a formální ověřování programů a systémů jsou:
Existují následující přístupy k formálnímu ověření:
Evidence-based programování je technologie používaná v akademických kruzích v 80. letech 20. století pro vývoj programů pro počítače s důkazy správnosti - důkazy o absenci chyb v programech (v rámci této teorie chyby chápány jako nesrovnalosti mezi koncipovaným algoritmem a skutečný algoritmus implementovaný programem).
Důkaz lze plně zautomatizovat jen pro velmi malý okruh jednoduchých teorií, proto se stává důležitým jeho automatické ověřování a k tomu i transformace do ověřitelné podoby. Značné množství prakticky důležitých problémů, včetně např. problému zastavení , je algoritmicky neřešitelných .
Aby se zachovala přísnost při kontrole důkazu ověřovatelem, měli byste zkontrolovat také ověřovatele, pro který je potřeba ještě jeden ověřovatel atd. Výsledný nekonečný řetězec ověřovatelů by se mohl zhroutit vytvořením samoověřovacího ověřovače, který má schopnost rozvinout se do praktického.