PlusCal is a tool for working with TLA+: it adds a pseudocode-like interface to the specs, making them easier for programmers to understand. While not every interesting spec can be written with PlusCal, quite a few can, and it’s a great entry point into modelling. All of the specs we’ll write over the course of this guide will run with PlusCal at the core.