GitHub repository: Beluga-lang/McTT
Primary language: Rocq Prover
Description: Building A Correct-By-Construction Proof Checkers For Type Theories