You write your Lean4 type-checker in a way that is amenable to formal proof. And then verify properties of your type-checker. Like Lean4Lean. https://arxiv.o

You write your Lean4 type-checker in a way that is amenable to formal proof. And then verify properties of your type-checker. Like Lean4Lean. https://arxiv.org/html/2403.14064v3 https://arxiv.org/html/2403.14064v3 https://github.com/digama0/lean4lean/tree/master https://github.com/digama0/lean4lean/tree/master