We design an invariance proof method for concurrent programs parameterised by a weak consistency model. This generalises Lamport/Owicki-Gries methods for sequential consistency. The calculational design of the proof method by abstract interpretation of a truly parallel semantics with separate communications restricted by a communication specification ensures soundness and (relative) completeness. We use the cat language to write specifications of consistency models as well as concurrent program specifications. We show how to design minimal program-specific communication specifications ensuring correctness which can be ported to different architectures by refencing.