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 seco