Formell verifiering
Matematiskt bevis att ett program uppfyller sin specifikation — tester visar att buggar finns, formell verifiering visar att de inte finns.
Proof assistants: Coq (numera Rocq, ~1989, Frankrike), Agda, Lean (Microsoft Research, drivit 2024-revolutionen i matte-bevis), Isabelle/HOL. Berömda bevisade system: seL4 (kärnan, 2009 — bevisad fri från en lång lista av klassiska kernel-buggar), CompCert (C-compiler, bevisad korrekt), Project Everest (verifierad TLS). Branta inlärningskurvor, månader till år för verifiering av enkla program — bara värt det för mycket säkerhetskritisk kod (luftfart, kärnkraft, krypto-bibliotek).