TLA is also a (linear) temporal logic that's simpler than LTL, and it's at the core of TLA+. If you don't want to spend months studying and then months writing

TLA is also a (linear) temporal logic that's simpler than LTL, and it's at the core of TLA+. If you don't want to spend months studying and then months writing proofs as a learning experience but rather would like to actually specify and verify real systems, use a language with a temporal logic model checker, like TLA+ (that has the TLC model checker) or Promella (Spin). If you want the other kind of experience, there have been implementations of TLA in both Coq and Isabelle.