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://github.com/digama0/lean4lean/tree/master