PlusCal (formerly called +CAL) is a formal specification language created by Leslie Lamport, which transpiles to TLA<sup>+</sup>. In contrast to TLA<sup>+</sup>'s action-oriented focus on distributed systems, PlusCal most resembles an imperative programming language and is better-suited when specifying sequential algorithms. PlusCal was designed to replace pseudocode, retaining its simplicity while providing a formally defined and verifiable language. A one-bit clock is written in PlusCal as follows: