Comment by miloignis

https://softwarefoundations.cis.upenn.edu/ is a great zero-to-hero resource (it's what I used), but to my knowledge it doesn't have an ecosystem review in it. It uses Coq, but the first book has been ported to at least Isabelle, if not others.