> Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).

Do you have to actually prove a tactic work for it to be sound? A tactic will rewrite the program into a simplified program that will verified by a kernel; if the tactic wrongly expands something, the kernel will later reject the program. Only the itself kernel need to be verified for the whole thing to be sound.

Or am I missing something?