You can only do so in another framework that might itself have bugs.

Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean".

The kernel does have bugs sometimes.