The following article is written by Andrius Velykis. The full link for the article is found below.

Z/EVES is an interactive theorem prover for Z notation. It can be used to develop Z specifications and reason about them. It has a number of attractive features, such as an easier learning curve (in comparison to related theorem provers, e.g. Isabelle), powerful proof tactics, and the ability to do proofs in Z notation.

http://andrius.velykis.lt/2012/09/installing-zeves-on-mac-os-x/

Z/EVES is an interactive theorem prover for Z notation. It can be used to develop Z specifications and reason about them. It has a number of attractive features, such as an easier learning curve (in comparison to related theorem provers, e.g. Isabelle), powerful proof tactics, and the ability to do proofs in Z notation.

http://andrius.velykis.lt/2012/09/installing-zeves-on-mac-os-x/