The first formal treatment of the semantics of Z was provided by Mike Spivey in his doctoral dissertation. This was published by Cambridge University Press as Understanding Z. Though this work does not cover the whole language (a crucial omission being set generic constructs), and is in some ways unnecessarily difficult to understand (e.g. in its handling of scope), it is still the most precise and intelligible semantic account available.
Since the early 90's a comprehensive formal semantics has been under development as a part of the Z standardisation process. Drafts of this standard are available from the Oxford University archive server.
Having watched this patch since starting work with Z in 1986, I became active early in 1990 because of my role in the development of ProofPower, particularly in the design of the features supporting proof in Z (background).
As a result of this work, I identified certain issues in relation to the semantics of Z which seemed to have impact on the feasibility of constructing formal machine checked proofs about specifications written in Z. These topics have also been discussed in the context of the Z standardisation process, and some of the changes I advocated are now incorporated in the draft standard.