This work builds on the tradition of hidden algebra which was started several years ago by Joseph Goguen. We extend the traditional hidden algebra formalism by a re-arrangement of the basic concepts. This re-arrangement of the hidden algebra formalism permits an extension to novel concepts which bring new practical strength to the specification and verification methodologies. The main novel concept, which constitutes the core of this work, is that of behavioural coherence, which is essentially a property of perservation of behavioural structures. We define this concept and study its main denotational and computational (including a special concept of term rewriting emerging from our approach) properties, and also show how the extension of hidden algebra with behavioural coherence still accomodates the coinduction proof method advocated by classical hidden algebra. The emphasize of this paper is however on the methodologies related to behavioural coherence. We present the basic methodologies of behavioural coherence by means of examples actually run under the CafeOBJ system, including many proofs with the system exiled to appendices.