I use lean a lot, reasonably effectively (although I’m still just getting started) but I’m using it as a proof assistant for mathematics. The background that is actually useful for understanding how lean works and most “mathematical” lean use cases is dependent type theory and homotopy type theory. So people who really want to go deep on lean often recommend the HoTT book (https://homotopytypetheory.org/book/) but that’s not required reading for getting started in lean, more like if you’re doing a PhD in formalization or whatever.

It sounds like for your use case of software verification mathematical logic is important, but that’s definitely not the case for most lean users. I wouldn’t say it’s required or even useful if you want to use lean for proving things in general.