米AT&Tのベル研究所で作られたソフトウェアです。
通信プロトコルの検証用途が発祥です。
NASAのDEEP SPACE 1 で適用した実績があるようです。

Promelaという記述言語を使用して、モデル検査を行います。
Promelaは、C言語に非常に近いです。モデルを詳細化しすぎると、ソースコードと同じくらいになってしまうかも・・・・