This is really neat, but in my opinion conflating theory and actual verification through Coq might be a bit too much for a newcomer. For those who are looking

This is really neat, but in my opinion conflating theory and actual verification through Coq might be a bit too much for a newcomer. For those who are looking for a softer introduction to the field, I highly recommend "Reactive Systems: Modelling, Specification and Verification" by Aceto, Ingólfsdóttir, Larsen, and Srba (full disclosure, I am a student at Aceto's current affiliation).