TLA+
TLA(Temporal Logic and Actions)
AWSのDynamoDB、EC2やS3（今はさらに増えている）といった数多くのサービスの仕様をこの言語で表記し、モデル検査によって矛盾や不整合がないかをチェックしているらしい 特徴は並行実行や分散システムをサポートしている
他の形式手法のツールに比べて数学的な素養があまりないプログラマーでも容易に習得ができるのが特徴
と言われているが自分はまだ習得できていない
TLA+では記述された仕様が正しいかをチェックするために、TLC Model Checkerというツールを提供している
参考
関連