PlusCal (formerly called +CAL) is a formal specification language created by Leslie Lamport, which transpiles to TLA+.
In contrast to TLA+'s action-oriented focus on distributed systems, PlusCal most resembles an imperative programming language and is better-suited when specifying sequential algorithms.
[1] PlusCal was designed to replace pseudocode, retaining its simplicity while providing a formally-defined and verifiable language.
[2] A one-bit clock is written in PlusCal as follows: This computer science article is a stub.
You can help Wikipedia by expanding it.