PlusCal (formerly known as +Cal) is an algorithmic language. It is designed to replace pseudocode. PlusCal can express both sequential and concurrent algorithms and features means to handle nondeterminism, atomicity and model checking.[1]
PlusCal expressions are written using TLA+.[1] The balance of PlusCal syntax can be translated to TLA+[2] for the purposes of debugging and model checking.