A MongoDB research team ran a second TLA+ workshop, this time integrating Claude Code as an AI assistant to lower the barrier to formal modeling. Unlike the first workshop two years prior, the AI-assisted format compressed instruction to under two hours and achieved dramatically higher conversion rates — nearly all attendees began modeling real work projects during the hands-on session. Key insights include: AI removes TLA+ syntax as a bottleneck, enabling focus on modeling concepts; a recommended workflow of design-first in TLA+ followed by LLM-generated code and model-based tests; best practices like avoiding PlusCal, starting with abstract minimal models (50–200 lines), and interviewing users before writing specs. The workshop also covered TLC model checking, temporal operators, and seven mental models for effective TLA+ use, including aggressive abstraction and deliberate atomicity splitting.
