I too know nothing about formal verification but I know that mathematical proof is different individual tooling. Informal statements, Lean and whatever other formal provers are all language and languages are social so what someone uses will impact you and so it's legitimate to have an opinion.