Формална верификация (Formal Verification)

Формалната верификация (Formal Verification) е математически метод за строго доказване на коректността на алгоритми, софтуерни програми или хардуерни интегрални схеми спрямо предварително дефинирани формални спецификации.

В ерата на AI асистентите формалната верификация през системи като Lean, Coq и Isabelle служи като краен съдия за валидиране на предложени от невронните мрежи математически теореми и критичен програмен код.