TLA+

TLA+ is a language for modeling software above the code level and hardware above the circuit level. The tool most commonly used by engineers is the TLC model checker, but there is also a proof checker.  TLA+ is based on mathematics and does not resemble any programming language. Most engineers will find PlusCal, described below, to be the easiest way to start using TLA+.

---- MODULE pluscal ----
EXTENDS Integers, TLC

(* --algorithm pluscal
variables
 x = 2;
 y = TRUE;

begin
  A:
    x := x + 1;
  B:
    x := x + 1;
    y := FALSE;
end algorithm; *)
====