TL;DR
2009 年に Leslie Lamport が開発したアルゴリズム記述言語。TLA+ をプログラマが使いやすくするために作られ、書いたアルゴリズムは TLA+ の仕様に変換される。
なぜ必要か
Lamport は、プログラミング言語は細かすぎる粒度で考えることを強いるので、並行処理について考えるのに向かないと述べている。並行処理のバグはコードを書く前にアルゴリズムの段階で直すべきだという考えである。PlusCal は特にマルチスレッドで実装するアルゴリズムを書いて検証するのに向いている。
仕組み
PlusCal で書いたアルゴリズムは、実行可能なコードにはコンパイルされない。代わりに TLA+ の仕様に変換され、TLA+ のツール（主にモデル検査器の TLC）で検証する。証明システムの TLAPS を使えば正しさを証明することもできるが、手間がかかるため、あまり行われない。