Formal verification
A mathematical proof that a program meets its specification — testing shows that bugs are present, formal verification shows that they aren't.
Proof assistants: Coq (now Rocq, ~1989, France), Agda, Lean (Microsoft Research, driving the 2024 revolution in maths proofs), Isabelle/HOL. Famously proven systems: seL4 (the kernel, 2009 — proven free of a long list of classical kernel bug classes), CompCert (C compiler, proven correct), Project Everest (verified TLS). Steep learning curves, months to years to verify simple programs — only worth it for highly safety-critical code (aviation, nuclear, crypto libraries).