The book Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers has been published by Addison-Wesley Professional, a division of Pearson Education. You can click here to order it from the publisher, or download a copy for your own use. You can also download accompanying material.
The BookThe book is 364 pages long (including a 17-page index). However, most people will want to read only the first part, which comprises the first seven chapters and is 83 pages long. Here is the list of chapters.
The List of CorrectionsThis is a list of all known errors and omissions in the book. If you are the first to report an error, you will be acknowledged in any new edition.
Accompanying MaterialAlso available for downloading is material to accompany the book. This includes the ASCII versions of all specifications from the book, additional modules and configuration files for using the TLC model checker to check some of the specifications, and a few exercises.
The material is organized hierarchically, with the material for each chapter in a separate folder (directory). Each folder, including the root, has a README file containing the exercises and an explanation of what else is in the directory. The material is available as a Zip file for Windows users and as a gzipped tar file for Unix users.