Формальная верификация
Математическое доказательство того, что программа соответствует спецификации: тесты показывают наличие ошибок, формальная верификация — их отсутствие.
Ассистенты доказательств: Coq (ныне Rocq, ~1989, Франция), Agda, Lean (Microsoft Research, двигатель революции в математических доказательствах 2024 года), Isabelle/HOL. Известные доказанные системы: seL4 (ядро, 2009 — доказано отсутствие длинного списка классических классов ошибок ядра), CompCert (доказанно корректный компилятор C), Project Everest (верифицированный TLS). Порог входа высок, на простую программу уходят месяцы и годы — оправдано только для критичного кода (авиация, атомная энергетика, криптобиблиотеки).