Learning TLA and Quint: verifying state transitions with Temporal Logic of Actions
What is it The other day I learned about TLA+, PlusCal, and Quint. TLA+ is a formal specification language that can be used to design, model, and verify software systems. As the name suggests (TLA: Temporal Logic of Actions), it is particularly well suited to describing state transitions and behaviors over time.
PlusCal is an algorithm language that is normally written inside a comment in a TLA+ module. Its syntax is more familiar to programmers who are used to imperative languages. The PlusCal translator converts it into TLA+, which can then be checked with the TLA+ tools.
