Interactive Learning Platform

Master Formal Verification
with TLA+ Quest

Learn TLA+ by completing hands-on formal verification challenges. Specify the algorithm, run the TLC model checker, and visualize the state space - all in your browser.

Start Solving Problems Create Account

See it in action

Visualize Every State Your System Can Reach

tla.quest/problems/bit-flags
TLA+ Quest state-space visualizer showing a solved bit-flags problem

Why TLA+?

Think more clearly
about your systems

Writing a TLA+ spec forces you to state precisely what your system does — every state, every transition, every assumption. That act of precision alone surfaces bugs before a single line of code is written.

Then TLC takes over, exhaustively checking every scenario you described. Race conditions, deadlocks, invariant violations — if they can happen, the model checker will find them.

MutexSpec.tla 
---- MODULE MutexSpec ----
VARIABLES state, owner

\* Safety: at most one holder
MutexOnlyHeldByOneThread ==
  \A t1, t2 \in Threads :
    (state[t1] = "held"
    /\ state[t2] = "held")
    => t1 = t2

INVARIANT MutexOnlyHeldByOneThread
==========================