Why not verify a Lean kernel with something other than Lean?