TLA+ Community Meeting 2023
Saturday, April 22, 2023
Paris, France

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.