Z is by far the most widely used formal specification notation, but it has provided quite a challenge for theorem proving as the language is rather complicated. A commercial version of HOL called ProofPower has been used to provide `industrial strength' proof support for Z. I have done some work on a more lightweight embedding of Z in HOL (see my ZUM' 94 paper for details).
Even more complicated than Z is Object-Z [6], an object-oriented extension of Z (there are several other object-oriented extensions of Z, and even a book on the subject [7]). Judging by messages in the news group ucam.cl.zforum, there would be quite a bit of interest in proof support for Object-Z, but maybe it is a bit premature to work on this before there is good support for pure Z!
A Z project that would be quite challenging, but also could be fun, would be to try to construct a deep embedding of Z in HOL-ST (see Section 3.7) based on the official semantics of Z in the Draft Standard.