Specify and model-check a small protocol with TLA+

Specify a lock service or two-phase commit, state its invariants, plant a bug, and explain the counterexample trace that TLC produces.

Not attemptedSelf-directed project (TLA+ tools)Access: free

Open resource

The exercise happens on Self-directed project (TLA+ tools). Canonical link: https://lamport.azurewebsites.net/tla/tla.html. Link check: link responded (5 Oct 2026). Opened from this app 0 times; opening is not counted as an attempt.

Supports: Awareness-to-working level formal reasoning for systems research and distributed-systems roles.

Record an attempt

OutcomeAttempted, not solvedSolved with help (hints, editorial or discussion)Solved independentlyReviewed an earlier solution

Date

Minutes (optional)

Language

Hints used

Confidence afterwards

Main mistake

Learning objective this practices (optional)

Notes (approach, bug, what to remember)

Re-attempt on (optional)

A date is suggested from the outcome.

Attempt history

No attempts recorded yet.