Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).