start

Welcome to the TLA+ Wiki

This wiki is community driven, and aims to become a useful resource for TLA+ users.

TLA+ is a high-level language for modeling programs and systems--especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.

TLC is a model checker for specifications written in TLA+.

----- MODULE HourClock -----
EXTENDS Naturals
VARIABLE hr
HCini  ==  hr \in (1 .. 12)
HCnxt  ==  hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC  ==  HCini /\ [][HCnxt]_hr
------------------------
THEOREM  HC => []HCini
=======================

----- CONFIG HourClock -----
(***************************************************************************)
(* This is a TLC configuration file for testing that HCini is an invariant *)
(* of the specification HC                                                 *)
(***************************************************************************)

SPECIFICATION HC
   \* This statement tells TLC that HC is the specification that it
   \* should check.

INVARIANT HCini
   \* This statement tells TLC to check that formula HCini is an
   \* invariant of the specification--in other words, that the
   \* specification implies []HCini.
======================

These are some of the ways you can contribute.

Wiki

Contributions to the wiki are very welcome!

To contribute you will need to register an account on this website (it only requires a username, email and password). Should you need it, TLA+ was created by Leslie Lamport.

You can learn the syntax from here. Markdown is not supported.

Tools

Currently the main areas are the TLC model checker (java), and the Visual Studio Extension.

If you're looking for some inspiration, be sure to check the monthly development update that usually has good first contribution ideas: https://foundation.tlapl.us/blog/index.html


Browse Topics:

  • start.txt
  • Last modified: 2025/07/15 17:51
  • by fponzi