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.