TLA+: The Tools, The Language, The Application Talk by Markus Kuppe, Microsoft Research

Abstract: TLA+ is a language for the formal specification and verification of discrete systems, including distributed algorithms. Users describe the system as a state machine, written in a language based on mathematical set theory and temporal logic that also serves to express safety and liveness properties. TLA+ comes with tools for computer-assisted verification, including two model checkers and an interactive proof system. TLA+ is used in academia and industry, e.g., to verify data consistency in cloud applications. This talk will cover the theory of TLA+ and how practitioners write TLA+ specs with the help of the verification tools. Afterward, we will discuss known limitations of the tools and outline current and future research opportunities.

Bio: Markus Kuppe is a Principal Research Software Development Engineer in the Research In Software Engineering group at Microsoft Research, Redmond. His focus is on making spec-driven development (with TLA+) more popular among engineers: This includes scaling verification to real-world problems and building tools to combine spec-driven development with established software engineering processes.