> 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

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