Z wasn't the first formal method I learned, nor was it the last, but it's surely one I like a lot, in the right situation. I learned it first at a summer school in 1986 held in Oxford and taught by members of the Programming Research Group. Much later I was a part of the ANSI standards committee charged with forming the US position on both Z and, also, the Vienna Development Method (VDM).
Z, in this context, pronounced Zed (like Rip Torn's character in Men in Black), is a formal notation (which really just means that there's a right way and many wrong ways to write it down) that's been used, primarily, to create models of software. It is named Z as short-hand for ZF which, itself, is short-hand for Zermelo-Fraenkel set theory which is the underlying basis for the notation.
If that's my definition, which I'll be the first to admit is quite a mouthful, what does it all mean and why would I care?
The Z notation can be used to specify software systems, by which I mean that it is possible to build a model of the system and reason (the verb form) about the system before any software is written. This doesn't sound exciting unless the system in question might be related to safety, something that if it failed could cause loss of life. The most extreme example of this would be that Z was used to model the software in a heart pacemaker. What makes the notation useful is that it can be simpler to build the model, so the incremental cost isn't outrageous.
As you might guess, the Z notation encompasses ZF set theory. But it also includes predicate calculus as a mechanism for writing expressions about sets. One of the most important parts, that makes specifications readable, is the schema calculus. This appears to be specialized forms of boxes but there is so much more to it than just being funny boxes.
A Z specification then becomes a collection of schemas. There are different types of schema. Some are used to describe the state space of the model, others are used to model how the state space changes. (OK, that's a bit of a lie; the underlying semantics are different, but that's a very deep discussion.) Finally there are schemas that are made up of combinations of other schemas (using the schema calculus).
Because it can be used in such an abstract way, Z is very powerful, the model doesn't have to be exactly the way software works - Z is used to model the what of what the system is supposed to do, not the how, so a lot of implementation details don't need to be written.
There are tools out there to help support writing Z specifications, fuzz and cadiz are tools I used to help format Z specifications as well as do some checking. Z-eves was a tool that could be used to create specifications and also prove theorems about the specifications. There was also a tool that I saw, but didn't use, from Australia that could perform a sort of execution of the specification - albeit very slowly.
There are a lot of good books out there about Z, however, I'd warn against one book. Not because the book is bad but because it has the most misleading title. It's called Understanding Z and was written by Mike Spivey. You'd think that would be a good book to understand Z. However, that's not quite the case. I've been told that it is a rewrite of Mike's D.Phil. thesis, which makes sense. The content of the book uses a Z-like notation to provide the denotational semantics of Z. If that sounds tricky, it is!