TLA+

Eiffel: Extending Formal Verification of Distributed Algorithms to Utility Analysis

This paper explores the use of TLA+ to verify game theoretic properties like Nash equilibria.

Arian Baloochestani Asl, Leander Jehl