TLA+
証明言語は、特定の定理証明者から独立するように設計されており、証明は宣言型で記述され、複数の個別の義務として変換されバックエンドの証明者に送信される。主なバックエンドの証明者はIsabelleとZenonであり、 SMTソルバーCVC3 、 Yices 、およびZ3定理証明者にフォールバックする。 TLAPSプルーフは階層構造になっているため、リファクタリングが容易になり、非線形開発が可能となる。前のすべてのステップが検証される前に、後のステップで作業を開始でき、難しいステップはより小さなサブステップに分解される。モデルチェッカーは検証が開始される前に小さなエラーをすばやく見つけるため、TLAPSはTLCとうまく連携する。同様にしてTLAPSは、有限モデル検査の機能を超えるシステムプロパティを証明できる。
TLAPSは現在、実数による推論も、ほとんどの時間演算子もサポートしない。 IsabelleとZenonは通常、算術証明の義務を証明できないため、SMTソルバーを使用する必要がある。 TLAPSは、ビザンチンPaxos 、Memoirセキュリティアーキテクチャ、およびPastry分散ハッシュテーブルのコンポーネントの正当性を証明するために使用されている。 これは他のTLAツールとは別に配布され、BSDライセンスの下で配布されるフリーソフトウェアである。 TLA、プルーフコンストラクトの言語サポートを大幅に拡張した。
上記の仕様では、1ビットクロックの奇妙な状態は許可されていないが、クロックが常に変化するとは言っていない。たとえば、次のような永続的なShuttering stepが起こりうる。
変化しない時計は役に立たないので、これらの振る舞いは禁止されるべきである。 1つの解決策はShuttering stepを無効にする事であるが、TLAでは常にShutteringを有効にする必要がある。Shuttering stepは、仕様に記載されていないシステムの一部への変更を表し、改良に有用である。最終的にTickしなければならないクロックを確保するために、弱い公平性がTickのためにアサートできる。
アクションに対する公平性が弱いということは、そのアクションが継続的に有効になっている場合は、最終的に実行する必要があることを意味する。Tickの公平性が弱いため、ティック間で許可されるShuttering stepの数は限られている。 Tickに関するこの時相論理ステートメントは、活性アサーションと呼ばれる。一般に、活性アサーションはマシンで閉じる必要がある。到達可能な状態のセットを制約するのではなく、可能な動作のセットのみを制約する必要がある。
ほとんどの仕様では、活性の表明は必要ない。安全性特性だけでモデル検査とシステム実装の両方に対して事足りる。
TLAの仕様は、ほとんどが通常の非時相論的数学で構成されていたが、Lamportは、純粋な時間的仕様よりも煩わしさが少ないと発見した。 TLAは、1999年に論文「Specifying Concurrent Systems with TLA」で紹介され、TLAの仕様記述言語としての数学的基礎を提供した。同じ年の後半に、YuanYuはTLA仕様のTLCモデルチェッカーを作成した。 TLCは、Compaqマルチプロセッサのキャッシュコヒーレンスプロトコルのエラーを見つけるために使用された。
ランポートは、2002年に「Specifying Systems:TLA Language and Tools for Software Engineers」というタイトルのに関する完全な教科書を発行した。 PlusCalは2009年に導入され 、TLAプルーフシステム(TLAPS)は2012年、 TLAは2014年に発表され、いくつかの言語構造が追加され、プルーフシステムの言語内サポートが大幅に増加した。 ランポートは、更新されたTLAのリファレンスである「The TLA Hyperbook」の作成に取り組んでいる。未完成な作品は彼の公式ウェブサイトから入手できる。Lamportは、TLA+ビデオコースも作成している。このコースでは、「プログラマーとソフトウェアエンジニアにTLA+コードの記述方法を教える入門から始まる一連のビデオレクチャーを作りかけている」と説明されている。