Why build Proof-Transport?
Formal proofs often “rot” when proof assistant kernels evolve (e.g. disabling Cut, tactic changes).
This forces re-verification at high cost.
Proof-Transport provides continuity: it re-compiles old proofs into new kernels and issues stability certificates.
