Formal verification

Mathematical checking that a solution meets a formally stated task and its pre- and postconditions: the task is written in a language such as Lean or Coq, and a verifier program checks the solution against it automatically.