In mathematics and software this usually means encoding a statement in a proof assistant such as Lean so a small trusted kernel accepts or rejects each step. A passing check shows the derivation is valid for the encoded statement. It does not by itself prove that the statement matches the informal theorem, regulation, or program you actually care about.