The specification and verification of shared-memory multiprocessor cache coherence protocols is a paradigmatic example of parallel technologies where formal methods can be applied. In this paper we present the specification and verification of a cache protocol and a set of formalisms which are based on ‘process theory’. System correctness is not established by simple techniques such as testing and simulation, but ‘ensured’ in terms of the underlying formalism. In order to manipulate the specification and verify the properties we have used an automated tool —namely the ‘Edinburgh Concurrency Workbench’ (CWB).