カリフォルニア大学／バークレー校で作られた、モデル検査用のソフトウェア。
スクリプトによって、ユーザ定義の関数を作成できる。

リアクティブなシステムの検査に適用できるらしいが、手作業が多い感じがする。