The formal object that a proof assistant checks to verify a proof is correct, distinct from the tactic script used to generate it.