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