They created an implementation of a Lean kernel in Lean (con-leche) and verified it as consistent.

Since there can be bugs in its compiler and runtime, they translated the code into Rust (con-ron), and verified the resulting kernel with another Rust-based verification tool.

There is also an ongoing verification project of Lean4, which is written in Lean4 itself. (My mental model is Lean4 := Raku and Lean := Perl)

So we have two verified kernels now, and another is awaiting release.

both