Dear Coq community,
I would like to start a discourse on the Coq kernel/checker, as in terms of logic it is probably the primary source of reliability of the tool, one of its distinguishing features and the one piece that I can find less public information about.
Apologies for verbosity, I tried to make every first sentence of each numbered item summarize the goal of the item it refers to.
I hope people of the community will further integrate or contribute to the following questions:
[Progression] Has the kernel/checker always been the same (say for a long time) or is it continuously evolving release after release?
If the latter holds then:
(A) How fast does the kernel evolve (compared to releases)?
(B) Do the revisions of the kernel undergo any meta-theoretical check over changes (e.g. that the implementation continues to implement CIC - or the underlying variant of CIC, when a implementation or meta-theoretical change occurs)? To be concrete with an example, it appears from the Credits section of the Coq reference manual  that version 8.9 of the kernel allows mutually recursive records, what level of trust is it built to make sure this addition does not break the kernel logical consistency?
[Documentation] Is there any place where information about the kernel implementation and its metatheory can be found?
Of course one could look into the kernel  or checker  implementations themselves, but I was rather wondering if the notorious “few pages metatheory” underlying Gallina syntax was otherwise available in written form as a complement - with, e.g., the corresponding proofs of safety, normalization, substitution lemmas, etc.
I know about Barras’ Coq in Coq , but that seems to be dealing only with CoC (plus I expect that the extracted kernel would not be able to deal with Gallina proof terms of today’s version of Coq).
Someone cited Coq’Art in the past (e.g. see the thread in ) but I do not know how complete is the treatment of that book with respect to implementation details - I do not have access to Springer.
Also  seems to be related but how close is it to the Coq kernel implementation?
From : “Gallina includes several useful features that must be considered as extensions to CIC. The important metatheorems about CIC have not been extended to the full breadth of the features that go beyond the formalized language, but most Coq users do not seem to lose much sleep over this omission”.
[Diversity] Is there only one implementation of the kernel/checker or are there more (e.g. cooked up using different programming languages, or preferring slower, more reliable versions vs. faster, optimized versions for fast QED)?
For example, in Lean there seem to be 3 officially available proof checkers , written in C++, Haskell and Scala (although 1 kernel for computing the terms ).
[Implementability] What would it take for people external to the Coq development team to implement a new kernel/checker from scratch?
Would it be just a matter of implementing CIC or would there be something more (e.g. dealing with Coq-specific constructs that are not part of CIC but are part of Gallina).
In  there are some details for how to build a small kernel for Matita, but I am not too confident that the information contained there are either to the point or enough for a complete implementation (e.g. dealing with modules for one thing).
This point is also related to that of [Documentation], above, and that of [Serializability], below.
[Serializability] Can Gallina terms generated by Coq be serialized in some tool-independent format, so that external tools can manipulate them?
A post on SerAPI recently came out  but I do not know whether there are any plans to make this or similar formats/APIs standard.
Lean seems to have such a feature .
[Minimality] Are there ways to use smaller parts of the small kernel to check the proofs generated by Coq (e.g. restricting the kernel to only deal with the CoC part, or using a subkernel with only one universe)?
The only approximation to this that I found (in ) seems to allow this partially using the options -norec and -admit of the
coqchkcommand (although I do not think it is to the point). Also compilation to .vio files seems to go in this direction but that just seems to remove opaque definitions.
It appears from e.g.  that efficiency reasons lead the developers to some larger-than-needed implementation of the Coq kernel, so I guess it would it be fair to imagine that less efficient implementations could lead to smaller kernels (I think of small in terms of code complexity, rather than kLOC). I am also wondering about how small a reliable kernel can be in order to be trusted (this is closely related to the point of [Documentation] above, if reviews of the kernel by external people are expected).
[Kernel vs. Checker] I am a bit confused about the separation of the Coq kernel and Coq proof checker.
coqchkseems to work on object .vo files, for which “non-logical information is not checked [by coqchk]” . Also, from the answer in  it seems that some information in lost while serializing to .vo files ("[…] there are many objects that are not serializable […]" and “[…] the checker inputs all the library information, but ignores quite a few datatypes.”)
So the question is: Is there any loss in using (and linking) .vo files (as opposed to relying on a “whole-program” compilation)?
coqchkactually use the same core code as
QEDdoes (or are these two checks performed by separate pieces of OCaml code)?
I am a non-expert with 100% trust in the Coq kernel, I am not proposing enhancements and neither am I trying to debunk Coq as a reliable system.
I just want to know more and start a discourse about the tool. I also have not read comprehensively all the works that I linked, so please apologize if I misread or misinterpreted something.
 A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. A compact kernel for the Calculus of Inductive Constructions. Sadhana, 34(1):71–144, 2009.
 jsCoq and SerAPI releases