Thanks for the book rec! Something that moves from Lamport's short, theoretical (but awesome) piece to concrete examples is exactly what I need. Will check it out.