keithadler 

An independent implementation of the Lean 4 kernel: expressions, universes, environments, type checking, definitional equality, inductive types, and quotients.

Reader for Lean 4 .olean files: memory-maps a compiled module and decodes its constants into Tenet kernel objects on demand.

Command-line checker for Lean 4 exports.

Reader for the Lean 4 export format and a driver that replays an export through the Tenet kernel.