TLA+ By Example

An interactive website for learning TLA+ through guided examples with an in-browser model checker.

Live at: tlabyexample.com

What is this

A Next.js static site that teaches TLA+ specifications through two sections:

1. Intro to TLA+ — step-by-step lessons on syntax, data structures, and TLC configuration
2. BlockingQueue Tutorial — an adaptation of Markus Kuppe's BlockingQueue tutorial, walking through a concurrent bounded buffer spec commit by commit

Each lesson has a split layout: explanation on the left, interactive playground on the right. The playground runs the TLC model checker directly in the browser via CheerpJ (TLA+ tools compiled to a JAR, executed in-browser).

Development

npm install
npm run dev       # start dev server at http://localhost:3000
npm test          # run jest tests
npm run build     # static export to out/

Requires Node.js 20+.