Concept

Formal verification

Establishing with a mechanical checker, such as the kernel of a proof assistant like Lean, that a statement or a program meets a precise mathematical specification.