Lean's proof checker is reproducible, and has been independently reproduced several times. See:

https://arena.lean-lang.org/