Note also that there is an independent checker https://github.com/leanprover/lean4checker https://github.com/leanprover/lean4checker to ensure that you're not p

Note also that there is an independent checker https://github.com/leanprover/lean4checker https://github.com/leanprover/lean4checker to ensure that you're not pulling any fancy tricks at the code level: that the compiled output, free of tactics, is in fact a proof.