What do you mean by a "recursion bug"? The terminology does not occur in the article so it seems to be a term that means something to you that is not very clear to me.
I am conflating (probably ignorantly) the idea in software development of bugs in recursive code, with the potential for bugs when using Lean to check Lean’s checker.
