Book Review: Practical TLA+

23 Nov 2018

Hey there. Lately, I got a chance to read Practical TLA+ by Hillel Wayne. I heard about formal specifications and TLA+ for some time already but never used it in any projects. It seemed to me as a type of tool that you use to check something either very non-trivial or involving concurrency (which is basically the same thing). After reading the book I feel this way even more.

The book starts explaining the syntax and semantics of TLA+ and PlusCal and proceeds with several examples of algorithms, data structures, and concurrent systems verification. Each chapter states the problem and starts with a simple spec that evolves into a more complex one as new conditions and possible failures are taken into consideration. It is quite easy to read if you still remember something from the set theory and logic; in case you don't, there is a short reference at the end of the book. The book is about 200 pages, contains a lot of code and screenshots; it took me a couple of evenings to read it.

In short, this is a good introductory book for the people interested in practical applications of formal specificactions and TLA+ particularly.