TLA+ Conf 2022
Thursday, September 22, 2022
St. Louis, MO, USA

The TLA+ Proof System

Jael Kriener, Tomer Libal, Tom Rodeheffer

TLAPS is an interactive proof environment for TLA+. Recent developments have focused on library modules, and on the addition of elementary temporal reasoning. The tutorial will present the current state of TLAPS and illustrate its use for verifying properties of TLA+ specifications.