After the soundness bug in the official Lean kernel found a few days ago (previously posted on this sub here https://www.reddit.com/r/math/comments/1va56l7/lean_4_bug_found_incidentally_by_ai_proving/), OpenAI approached Leonardo de Moura with their internal cybersecurity model and found 6 more soundness bug in the official kernel, see the section "What the FRO is doing" in https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/
All of these were not reproducible in the alternative typechecker for Lean 4, nanoda.