Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.