Rocq kernel

Tools: Rocq (formerly Coq)

• (Compiler implementation) The trusted core of Rocq that type-checks proof terms against the Calculus of Inductive Constructions, ensuring all accepted proofs are valid.