Why do you name Lean here as opposed to the other provers? Lean is "the new shiny thing" but my impression is that the community sees its focus in math, not so much software verification.
Quite a few design decisions (e.g. focus on classical reasoning support, focus of existing libraries) suggest that software verification of Lean programs isn't seen as a major application. (Of course you can always define a framework and prove stuff about C programs, like the "software foundations" book illustrates in Coq. But that's not really something new and again would need a lot of foundational work and tooling, essentially duplicating what people do with Coq, for no obvious benefit).