PlusCal

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:

-- fair algorithm OneBitClock {
  variable clock \in {0, 1};
  {
    while (TRUE) {
      if (clock = 0)
        clock := 1
      else 
        clock := 0    
    }
  }
}