[nextaccountic]

> 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?

[kmill]

You're not missing anything. I was going to mention this but decided not to get into it. (One detail: you can't verify the kernel exactly because of Gödel incompleteness issues.)