Correct by Design with TLA+

Human cognition is optimized for sequential reasoning, but many of the engineering challenges we face as designers involve many concurrent moving pieces. Examples include lockless data structures, distributed algorithms, OS task schedulers, and more.

Traditional testing methodology such as unit or integration testing only proves correctness for part of the system the test covers. How does the designer prove the system works correctly under all scenarios?

This book explains how designers can use TLA+ and model checker to describe and verify the correctness of a design. TLA+ is a system specification language that allows the designer to describe a system as a set of states, and specify invariants a state or a sequence of states must hold during runtime. The model checker exhaustively explores all possible states permitted by the spec to ensure invariants are upheld under all scenarios. A model checker verified TLA+ spec provides the designer with very high confidence in its correctness.

Fortunately, the core TLA+ language semantics is pretty manageable. This book will cover a selection of TLA+ examples to enable the readers to quickly get familiar with this wonderful tool.