The authors have a great deal of experience using the specification language TLA+ and its model checker TLC to analyze protocols designed at Digital and Compaq (both now part of HP). The tools and techniques the authors have developed apply equally well to software and hardware designs. This paper describes the authors’ experience using TLA+ and TLC to verify cache-coherence protocols.