TLA+とは - TLA+メモ@ウィキ

TLA+とは

TLA+（Temporal Logic of Actions）は、Leslie Lamportが開発した形式手法の一種です。
形式手法とは、ソフトウェアシステムを数学的にモデル化し、その正確性や信頼性を検証するための手法です。
具体的には、TLA+は、システムの振る舞いを表現するための仕様記述言語であり、システムがどのような状態にあるかを表す「状態」、状態がどのようなイベントによって遷移するかを表す「アクション」、そしてアクションが実行される順序を表す「時間」を扱うことができます。
Leslie Lamport氏は2024年12月にTLA+の開発から引退し、TLA+はTLA+ Foundationの元で開発が続けられています。