Compiler correctness is an old problem that has received renewed interest in the context of \emph{smart contracts} — that is, compiled code on public blockchains, such as Ethereum or Cardano, that often controls significant amounts of financial assets and can no longer be updated once it is committed to the blockchain. This paper discusses the design and implementation of a certifying compiler for the Plutus smart contract system using the Coq proof assistant.