Just noticed this - although
A Science of Concurrent Programs has long been available for free
on Lamport's website, it is now officially published by Cambridge in hardcover & ebook form!
Have people been reading it? Personally I have read up to section 6.3, the presentation of the Paxos algorithm as a hierarchical refinement of TLA+ specs (basically another presentation of Lamport's Turing Award lecture). I have stalled out there but recently Alex Kladov has been posting
comments about Paxos on lobste.rs, specifically about how going through this presentation really solidified his knowledge about why Paxos works instead of it just being an elegant method of dodging all the stuff that can go wrong, which is how I usually think of it. So I think I will try to read through it in the near future.