TLA+
ランポートは、スーザンオウィッキが主催したスタンフォードでの1978年のセミナーで、プヌーリのLTLに最初に遭遇しました。ランポートによると「時相論理は、実用化されそうもなく抽象的で無意味だと確信していたが、楽しそうだったので参加した。」 との事であったが、1980年に彼は「'Sometime' is Sometimes 'Not Never'」を出版し、時相論理の文献で最も頻繁に引用される論文の1つとなった。 ランポートは、SRI在籍中に時相論理仕様の作成に取り組んだが、このアプローチは実用的ではないとわかった。
彼が実用的な仕様方法を模索した結果として1983年に論文「Specifying Concurrent Programming Modules」が生まれた。この論文では、状態遷移をプライム変数と非プライム変数のブール値関数として記述するというアイデアが導入されている。 その模索は1980年代に継続され、ランポートは1990年にアクションの時相論理に関する論文群の発表を開始した。しかし、1994年に「アクションの時相論理」が発表されるまでは正式には導入されなかった。 TLAは、時間式でのアクションの使用を可能にした。これは、ランポートによれば、「並行システム検証で使用されるすべての推論を形式化および体系化するための洗練された方法を提供する。」とされている。