Our MongoDB TLA+ Workshop

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…