We are happy to announce release 1.0 of the MetaCoq project for Coq 8.14, 8.15, and 8.16, available both as sources and as opam packages. See the website for a detailed overview of the project, introductory material and related articles and presentations. MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, correct and complete type checker for PCUIC, and a verified type and proof erasure procedure from PCUIC to untyped lambda calculus. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself. You can install MetaCoq directly from sources or by typing opam install coq-metacoq. This release will also be included in an upcoming Coq Platform. The current release includes several subpackages, which can be compiled and installed separately if desired: the Template-Coq quoting library (in directory template-coq and as coq-metacoq-template) a formalisation of meta-theoretical properties of PCUIC, the calculus underlying Coq (pcuic / coq-metacoq-pcuic) a total verified type-checker for Coq (safechecker / coq-metacoq-safechecker), usable inside Coq or extracted to OCaml as MetaCoq SafeCheck <term> a verified type and proof erasure function for Coq (erasure / coq-metacoq-erasure), usable inside Coq or extracted to OCaml as MetaCoq Erase <term> a set of example translations from Type Theory to Type Theory (translation/ coq-metacoq-translations). A good place to start are the files demo.v, safechecker_test.v, erasure_test.v in the test-suite directory. MetaCoq is developed by Abhishek Anand, Danil Annenkov, Jakob Botsch Nielsen, Simon Boulier, Cyril Cohen, Yannick Forster, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau, and Théo Winterhalter. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available. The MetaCoq Team