What does “verified” mean here? Someone has formalized verified the kernels or just different kernels cross check each others?
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.
It's a marketing post at the end of the day is what I'm trying to say. Regardless, Lean is probably the most trustworthy proof assistant on the planet at this point.
Programming as a hand-crafted art is really diminishing fast.
Isabelle/HOL is probably at similar footing to Lean because its kernel is so simple.
It seems no one understands how useless this theorem is in practice.