It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain.

However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language.

Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.