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 metatheoretical check over changes (e.g. that the implementation continues to implement CIC  or the underlying variant of CIC, when a implementation or metatheoretical change occurs)? To be concrete with an example, it appears from the Credits section of the Coq reference manual [1] 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 [2] or checker [3] 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 [4], 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 [5]) 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 [6] seems to be related but how close is it to the Coq kernel implementation?
From [7]: â€ś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 [8], written in C++, Haskell and Scala (although 1 kernel for computing the terms [9]). 
[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 Coqspecific constructs that are not part of CIC but are part of Gallina).
In [6] 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 toolindependent format, so that external tools can manipulate them?
A post on SerAPI recently came out [10] 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 [11]. 
[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 [12]) seems to allow this partially using the options norec and admit of thecoqchk
command (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. [13] that efficiency reasons lead the developers to some largerthanneeded 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.
Commandcoqchk
seems to work on object .vo files, for which â€śnonlogical information is not checked [by coqchk]â€ť [12]. Also, from the answer in [14] 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 â€śwholeprogramâ€ť compilation)?
And doescoqchk
actually use the same core code asQED
does (or are these two checks performed by separate pieces of OCaml code)?
I am a nonexpert 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.
[1] https://coq.inria.fr/refman/credits.html
[2] https://github.com/coq/coq/tree/master/kernel
[3] https://github.com/coq/coq/tree/master/checker
[4] https://github.com/coqcontribs/coqincoq
[5] https://sympa.inria.fr/sympa/arc/coqclub/201305/msg00071.html
[6] 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.
[7] http://adam.chlipala.net/cpdt/html/StackMachine.html
[8] https://github.com/leanprover/lean/blob/master/doc/faq.md
[9] https://github.com/leanprover/lean/tree/master/src/kernel
[10] jsCoq and SerAPI releases
[11] https://github.com/leanprover/lean/blob/master/doc/export_format.md
[12] https://coq.inria.fr/refman/practicaltools/coqcommands.html
[13] https://sympa.inria.fr/sympa/arc/coqclub/201309/msg00082.html
[14] https://stackoverflow.com/questions/48849091/howisavofilestructuredsothatcoqchkmayuseit