[nextos]

However, the amount of teaching material focusing on software verification using Lean is frustratingly small?

Coq has FRAP and CPDT [1], which teach you most techniques that are used in industry. Also Software Foundations.

AFAIK, there's a version of Concrete Semantics using Lean [2]. But that's still just semantics.

Any other materials focused on software verification, not on formalizing mathematics?

[1] http://adam.chlipala.net

[2] https://news.ycombinator.com/item?id=22794533

[kevinbuzzard]

Yes. Coq has been around for decades and was adopted by the software verification community. Lean is much younger and its mathematics library caught on with the mathematician crowd, meaning that much of the Lean documentation right now is focused on mathematics. The hitchhiker's guide to logical verification https://cs.brown.edu/courses/cs1951x/static_files/main.pdf is a book more suited for programmers, although it is in Lean 3 and right now the community is migrating to Lean 4.