TLA+ Formal Specification Skill

Write non-trivial TLA+ specifications, run the TLC model checker, and bridge the gap between formal specs and implementation code.

Setup (Run Once)

bash SKILL_DIR/scripts/setup.sh

This downloads tla2tools.jar (v1.8.0) and verifies Java 11+. The JAR is stored at SKILL_DIR/lib/tla2tools.jar.

Quick Reference

Load the right reference for your task: