TLA+
レスリー・ランポートによる並行システム向けの形式仕様記述言語。システムが何をすべきかを書けば、モデル検査器が不正な状態に陥らないことを検証してくれる。
基礎は行動の時相論理（temporal logic of actions）。モデル検査器TLCは、取りうる状態遷移をすべて網羅的に探索する。Amazon Web ServicesはS3、DynamoDB、EBSの設計に使い、実装に入る前に設計上のバグを見つけた。MongoDB、Cosmos DB、Microsoft Azureも利用している。学習曲線は急で、教科書（Specifying Systems）をランポート本人が書いているほどだ。競合のチェッカーにApalacheがある。PlusCalは擬似コード風の構文で、TLA+へ変換される。