Precise behavioral models · Formal specification language
TLA+
Model possible system behaviors and state the properties those behaviors should satisfy.
What it helps you do
Inspect design-level behavior that can be difficult to see in individual code paths, particularly interleavings and state changes.
Starting knowledge: Comfort with sets, logic, state transitions, and concurrent behavior is useful.
- Define the relevant state and initial condition.
- Describe allowed next-state actions.
- State safety and liveness properties with the assumptions needed to assess them.
The problem it came from
Leslie Lamport created TLA+ as a mathematical language for specifying systems, especially concurrent and distributed ones. Its foundations use states, actions, and temporal logic.
The TLA+ tool ecosystem includes the TLC model checker and TLAPS proof system. Writing a model, exploring a bounded configuration, and proving a theorem are different activities.
Work through an example
Conceptual trace:
Initial: capacity = 1, reserved = 0
Worker A checks: reserved < capacity
Worker B checks: reserved < capacity
Worker A reserves a place
Worker B reserves a place
Result: reserved = 2
Intended invariant: reserved <= capacity
Model the check and update as separate actions if the implementation permits that interleaving.- The trace illustrates a safety failure, not an actual model-checker result.
- Combining check and update into one modeled action could hide the race.
- A real specification needs an explicit state model and a checked configuration.
Where it helps. Where it stops.
Use it when
- Several actors or retries can interact in unexpected orders.
- A design needs a precise model before implementation or a counterexample to a proposed invariant.
Potential benefits
- A model can expose a trace that violates an intended property.
- Explicit assumptions make the scope of a check discussable.
Limits and common mistakes
- A model can abstract away the bug you care about.
- A bounded TLC run is not a proof about every deployment, and this website does not run TLC.
The prompt below asks for this structure. It does not guarantee accuracy, complete coverage, better learning, or conformance to a standard. Treat those outcomes as separate checks.
Practise the judgment
Try a choice, inspect a boundary, then explain a case yourself. Hints and answers are available whenever you need them.
Which property is a safety invariant for workshop capacity?
Hint
Think “the bad thing never happens.”
Explained answer
Best answer for this case: No reachable state has more reservations than capacity
A safety property rules out a bad state or behavior. Eventual progress is a different kind of property.
A model makes check-and-reserve atomic, but the implementation separates them. What is the risk?
Hint
Check which behaviors the model excludes.
Explained answer
Best answer for this case: The model may hide a real race
The abstraction removes an interleaving that the implementation permits.
What evidence should accompany a claim that an invariant passed TLC?
Hint
What would another reviewer need to repeat the check?
Explained answer & self-review rubric
Record the exact specification, configuration and bounds, tool version, command, and actual result. Explain the modeled assumptions and omitted behavior. Do not describe a handwritten trace as a TLC run.
- Identify the checked artifacts
- State bounds and assumptions
- Retain actual tool evidence
Take it into your own work
Manual template
Use this structure yourself, with a colleague, or in your preferred writing tool.
# Behavioral specification brief
State variables:
Initial condition:
Allowed actions:
Concurrency and failure assumptions:
Safety invariants:
Liveness requirements and fairness assumptions:
Model-checking bounds or proof obligations:
Observed result and counterexample trace:
Abstractions not covered:
Review the result
- Does the model retain relevant interleavings?
- Are checking bounds and assumptions recorded?
- Is a tool result distinguished from a handwritten trace?
Use this approach with your own AI tool
Help me apply TLA+ to the material below.
Reader and existing knowledge: [describe]
Task and desired outcome: [describe]
Use these principles: Define the relevant state and initial condition.; Describe allowed next-state actions.; State safety and liveness properties with the assumptions needed to assess them..
Preserve source facts, identifiers, quantities, conditions, exceptions, and uncertainty.
Separate supplied facts from assumptions. Ask for missing information instead of inventing it.
Explain your representation choices and provide a review checklist. Do not claim formal compliance or correctness from formatting alone.
Material: [paste only information you are permitted to share]Go to the source
History and the underlying approach are grounded in these references. Examples, prompts, and practice cases here are original educational adaptations. Edition-specific details should be checked against the referenced publication.
Last editorial review: 2026-10-24. An overview is not certification, and this guide is not a reproduction of a standard.