The complete book of TLA+. The first seven chapters (83 pages) are a rewritten version of . That and the chapter on the TLC model checker are about as much of the book as I expect people to read. The web page contains errata and some exercises and examples. This book will teach you how to write specifications of computer systems, using the language TLA+. It’s rather long, but most people will read only Part I, which comprises the first 83 pages. That part contains all that most engineers need to know about writing specifications; it assumes only the basic background in computing and knowledge of mathematics expected of an undergraduate studying engineering or computer science. Part II contains more advanced material for more sophisticated readers. The remainder of the book is a reference manual| Part III for the TLA+ tools and Part IV for the language itself.