Wouldn't a bug in the (Lean) kernel just result in a PR to Lean?