The 6.822 page[1] has a draft[2] of Adam Chlipala's "Formal Reasoning About Programs", "introducing both machine-checked proof with [Coq] and approaches to formal reasoning about program correctness".

[1] https://frap.csail.mit.edu/main [2] http://adam.chlipala.net/frap/frap_book.pdf