Coq is an interactive theorem prover developed initially at and now with key support of INRIA for more than 38 years. Its current major version 8.x was released 18 years ago. Contrary to other proof assistants, an explicit design goal of Coq is to preserve backwards compatibility as much as possible, to make it easy for the community to support the millions of lines of verified code written. As a side effect of this, the kernel of Coq as of today comprises 18k lines of (OCaml) code. In average, one critical bug (i.e., one proof of falsity) occurs in Coq per year. Extensions of the system and both noncritical as well as critical bug fixes have to ensure that efficiency of the kernel is maintained and soundness not affected: a highly non-trivial task for such a big system.

MetaCoq provides a formalisation of large parts of Coq’s type theory in Coq and verified implementations of crucial parts of Coq’s kernel. In the past, attempted correctness proofs in MetaCoq have unveiled bugs in Coq’s kernel. In the present, the MetaCoq team, consisting of 12 people and several interns, is working on including all aspects of Coq’s type theory in MetaCoq. In the future, we hope that extensions of Coq’s type theory are first implemented as an extension of MetaCoq and proved correct, and only then the implementation of the kernel is changed.

Thus, maintaining an implementation of Coq verified in Coq as part of MetaCoq can help anticipating and preventing unsoundness and other problems before they make their way into the kernel.