Biçimsel doğrulama (formal verification)
Bir programın belirtimini karşıladığının matematiksel kanıtı: test hataların var olduğunu gösterir, biçimsel doğrulama ise olmadığını.
Kanıt asistanları: Coq (artık Rocq, ~1989, Fransa), Agda, Lean (Microsoft Research; 2024'te matematik kanıtlarındaki devrimi sürükledi), Isabelle/HOL. Kanıtlanmış ünlü sistemler: seL4 (çekirdek, 2009; uzun bir klasik çekirdek hata sınıfı listesinden arınmış olduğu kanıtlandı), CompCert (doğruluğu kanıtlanmış C derleyicisi), Project Everest (doğrulanmış TLS). Öğrenme eğrisi diktir; basit programları doğrulamak aylar, hatta yıllar sürebilir. Bu yüzden yalnızca güvenlik açısından çok kritik kod (havacılık, nükleer, kripto kütüphaneleri) için değer.