# Our MongoDB TLA+ Workshop > Source: > Published: 2026-06-13 13:23:23+00:00 Shortly after I joined MongoDB research, we ran a TLA+ workshop. It was a two-day ordeal. We had a 1.5 days of instruction on TLA+ and syntax, after which we tried to help people get started with modeling. People liked learning about TLA+ on the first day, but except for a person or two, we didn't get anyone onboarded with TLA+ modeling. It was too much to offload on people and ask them to level up in a short time frame. Well, two years after that first workshop, on May 11th, 2026, we ran a second edition of this workshop with one very big difference. What is that big difference, you ask? AI! AI makes formal methods not only necessary, but also more feasible and easier! Jesse, Will, and I planned this workshop to be aggressively short. We provide under two hours of instruction, then everyone starts modeling hands-on. We act as TAs and help people as they go. The AI takes care of the syntax problem for TLA+, and also helps with modeling. We just need to teach people enough to read and make sense of a model, and Claude Code would take care of the rest. You have a problem? Ask Claude. Still stuck? Ask us. Ok, I will cut to the chase. The workshop was a great success! My biggest takeaway from it is this: I finally see a green path to 100 true fans. We had an order of magnitude greater conversion rate compared to the first workshop. Almost all of the attendees got started with modeling, and almost all of those modeled a part of an actual work project they are currently on. As I've written before, with AI tools it is easy to be "technically fearless." People who had been heavy Claude users did a great job prompting and interacting with Claude, and hit the ground running. Some people were still hesitant to take the first step, but when one of us sat down with them, they quickly got over that initial friction and were off and modeling within minutes. We asked attendees to fill out a feedback survey afterward, and the results were encouraging. Across the board, attendees rated the workshop a 5 out of 5 and strongly agreed that TLA+ is a valuable tool for ensuring system correctness. Several attendees reported modeling real, current work projects during the hands-on session (including a concurrent rewrite of a core subsystem, a data materialization pipeline, and a distributed storage component) and found the exercise revealed liveness issues and design ambiguities they hadn't previously articulated. One attendee described how modeling gave them confidence in a design they would otherwise have had to validate the hard way through implementation. On the question of AI integration, the feedback was uniformly positive. Multiple respondents noted that Claude Code removed syntax as a barrier entirely, letting them focus on the modeling itself rather than fighting the language. One participant said: "I have tried to write TLA+ pre-LLMs, and it was prohibitively difficult." Likelihood-to-use scores ranged from 3 to 5, with most landing at 4 or 5. The most common suggestions for improvement centered on adoption strategy: how to make TLA+ part of the default design workflow for engineers who aren't yet in the habit, perhaps through a champion system similar to what MongoDB has done with AI tooling. At the workshop, we brainstormed what a best-practices guide for AI-assisted TLA+ modeling should look like. Here is what we landed on. No PlusCal! Stick to TLA+ directly. Keep it simple, easy to read, guarded commands. This is something I changed my mind on about three years ago, and I'm now happy to see that with AI assistance, there is no need to detour through PlusCal. As a mnemonic: /\ is like ∩ (intersection), so it means "and"; \/ is like ∪ (union), so it means "or." Always include a .cfg file with the same name as the spec. Before writing a single line, interview the user: (This is a bit tongue-in-cheek.) Pretend you are Lamport. Be brutally minimalist, and only add things if you can show they are relevant. Start from the most abstract model possible. Only go more concrete if you need to, and consult the user when you do. Initially aim to stay within 50–200 lines. A model that stays small forces you to think clearly about what matters. Prevent cognitive debt: explain each action with a short comment, so the reader can follow the intent without reverse-engineering it. I opened with a motivational overview of modeling, drawing on my [previous](https://muratbuffalo.blogspot.com/2018/01/why-you-should-use-modeling-with.html) [posts](https://muratbuffalo.blogspot.com/2018/10/debugging-designs-with-tla.html). The core message was this: as AI models write more of our code, formal modeling for concurrent and distributed systems is becoming more valuable than ever. TLA+ is not just a verification tool. [It is a design accelerator.](https://muratbuffalo.blogspot.com/2026/03/tla-as-design-accelerator-lessons-from.html) It shifts your perspective: forces you to think about the system globally, lets you explore alternative designs quickly and safely before any code exists. It is faster to fix a conceptual model than to whack-a-mole corner cases in implementation. And thanks to LLMs, learning TLA+ syntax is no longer the bottleneck. AI and TLA+ amplify each other. The workflow I described: I reinforced the message that AI + TLA+ is a massive win for the future of software development. I also introduced a distinction I find underappreciated: [the difference between modularity abstraction and modeling abstraction.](https://muratbuffalo.blogspot.com/2026/05/the-two-abstractions-of-system-design.html) Modularity abstraction hides implementation details through encapsulation and layering (the traditional approach taught in CS curricula). Modeling abstraction does something different: it reduces a system to its essential behavioral elements by stripping away everything irrelevant to the properties you want to study. While modularity abstraction aspires to conceal concurrency, modeling abstraction deliberately exposes it to maximize safe parallelism. The key skill in formal methods is knowing how to model abstractly (deciding on what to throw away) which is fundamentally different from the modularity thinking that programmers already have. [Jesse gave an introduction to TLA+ grounded in its computational model pitched for the LLM era.](https://emptysqua.re/blog/intro-to-tla-plus-for-the-llm-era/) He started from the transition model: a TLA+ spec defines a state machine through three pieces: an initial-state predicate describing valid starting configurations, a set of actions (state-transition rules) that define legal moves, and fairness constraints that ensure the system makes progress rather than stalling forever. Each state is a complete assignment of values to the variables, and a behavior is a sequence of such states. Jesse walked through [the coffee beans example](https://learning.tlapl.us/specs/CoffeeCan/) to show how guards (preconditions) and next-state assignments work together. He then explained how TLC, the TLA+ model checker, verifies specs by doing breadth-first search through the reachable state graph, exhaustively exploring all possible behaviors that the spec allows. This is what makes TLA+ different from testing: you are not sampling executions, you are covering all of them (up to the model bounds). Temporal operators like □ ("always") and ◇ ("eventually") let you express properties about entire infinite behaviors, not just individual states. The punchline Jesse made was again this: In the LLM era, you don't need to memorize the syntax to do this. You only need to understand what you are asking the model to check. Will Schultz walked through a realistic data cloning specification, defining key properties formally and showing how to think about correctness in a domain most of the attendees work in daily. He then demoed [Spectacle](https://github.com/will62794/spectacle), his tool for interactive spec exploration and visualization — letting attendees see the state space as a navigable graph rather than a wall of output. He also covered the current state of AI-assisted modeling workflows with TLA+, grounding the "Claude can help" claim in actual practice. Then we did the hands-on portion. Attendees picked a current work project, and we worked with them as TAs. That's where the real learning happened of course! I closed the workshop by pointing people at where to go from here, and tried [to give them a map of the conceptual territory](https://muratbuffalo.blogspot.com/2026/03/tla-mental-models.html) for leveling up. Effective TLA+ modeling rests on seven interconnected mental models. The foundation is aggressive abstraction: knowing what to discard rather than what to include. Paired with that is embracing TLA+'s global shared-memory fiction as a powerful reasoning tool rather than fighting it as unrealistic. From there, three refinement techniques: localizing guards to stable predicates (which makes slow models fast), deriving tight invariants that reflect genuine understanding of the system, and splitting atomic actions deliberately to expose real-world concurrency. These help you deepen a model until it tells you something you didn't already know. Beyond correctness verification, these mental models serve a critical communication function. A well-written TLA+ spec is precise and executable documentation. It keeps distributed teams aligned on design intent in a way that English prose cannot. By exploring protocol alternatives through stepwise refinement and varying atomicity levels, teams can discover optimizations they wouldn't find through implementation alone.