One of the central claims of fame of the Coq proof assistant is extraction, i.e. the ability to obtain efficient programs in industrial programming languages such as OCaml from programs written in Coq’s expressive dependent type theory, used, amongst many others, in the CompCert project.

For executables obtained by extraction, the extraction process is part of the TCB, as are Coq’s elaboration and kernel, and the compiler used to compile the extracted code.

The MetaCoq project aims at decreasing the TCB of Coq’s kernel by re-implementing it in Coq itself and proving it correct w.r.t. a formalisation of Coq’s type theory in Coq.

We aim at taking one step further, namely removing the extraction process from the TCB as well. Our goal is to provide a verified drop-in replacement for Coq’s extraction process to OCaml. To be able to start with a trustworthy and economic specification, we extract to the intermediate language of the OCaml compiler as specified in the Malfunction project.

We report on our ongoing effort to verify the operational correctness of the obtained programs.