Function check_derivation 

pub fn check_derivation(
    premises: &[ProofExpr],
    goal: &ProofExpr,
    derivation: DerivationTree,
) -> VerifiedProof

Certify and kernel-check a derivation built EXTERNALLY (e.g. by the fast grid solver) against premises ⊢ goal, WITHOUT running the backward chainer. The trust guarantee is identical to prove_certify_check: verified is true only when the certifier produced a kernel term whose inferred type IS the goal type. So an external solver sits OUTSIDE the trusted base — it hands us a DerivationTree, the kernel re-checks it, and a wrong tree yields verified == false, never a false claim.