If there's concern, I understand Lean can dump out a proof object, and this object can be checked for validity by a separate, smaller program. One could even write that smaller program multiple times.

It would be interesting to see how Lean is being tested. Pummeling it with inputs from AI proof search engines sounds like a good way to expose hidden bugs, just as pummeling a compiler with randomly generated programs is a good way to expose previously unknown compiler bugs.