Not the author but a recent book I've read on the subject served as a gentle introduction for me: The Little Prover [0]. If you can get past the lisp syntax you can get through this book with an informal and incomplete education in set theory and an intuitive understanding of logic.

[0] https://mitpress.mit.edu/index.php?q=books/little-prover

Lamport's tutorial (the TLA+ Hyperbook) as well as the old TLA+ book (Specifying Systems) -- both available freely on the TLA+ homepage -- cover all the math you need (which is little more than logical conjunction/disjunction/implication, the quantifiers for all/exists, and set membership/union/intersection). But it is perhaps better to be familiar with those simple concepts beforehand, although note that what you need is very, very basic. As nmrm2 said, there's no need for a full Discrete Math course (or a whole book).

If you have had the equivalent of an undergraduate course on Discrete Mathematics you are probably fine; an introduction to logic course (covering e.g., soundness and completeness of propositional/first order logics) probably isn't necessary.

There is a self-contained book; IMO chapter 1 gives a good overview of what you should be comfortable with:

http://research.microsoft.com/en-us/um/people/lamport/tla/bo...