Leslie Lamport Last modified on 10 August 2021 You'll miss a lot on this web site unless you enable Javascript in your browser. Introduction [show] TLA+ is a language for modeling software above the code level and hardware above the circuit level.  It has an IDE (Integrated Development Environment) for writing models and running tools to check them.  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 re...