Various attempts at supporting proof in Z are described in the literature. We survey some of these, together with the underlying semantic issues which make proof in Z a non-trivial task. Special care is given to an account of the peculiarities of Z schemas. The proof tools surveyed divide into two groups: custom-made implementations for supporting Z, and encodings of a Z logic within some other logical framework. The latter are further subdivided into `deep' and `shallow' embeddings. The broad conclusion is that none of these approaches is a clear winner at present, but that each may be able to benefit from the others.