Modeling Distributed Systems with Quint (and a bit of TLA+)

Join us online for an exploration of Quint, a modern language for modeling and reasoning about distributed systems, and how it relates to TLA+ and other formal specification tools.
We’ll start with a guided introduction to Quint’s design and syntax — what problems it solves, how it differs from TLA+, and how it helps express complex distributed behaviors clearly and precisely.
What we’ll cover:

• 🧩 What is Quint?
  A practical modeling language inspired by TLA+, designed for composability, strong types, and developer-friendly syntax.
• ⚙️ Modeling Distributed Systems
  Describe safety and liveness properties, model concurrent transitions, and reason about correctness.
• 🔄 Comparing Quint and TLA+
  When to use which, and how Quint builds on TLA+ ideas while simplifying everyday use.
• 🧠 Hands-On Practice
  Try modeling a small distributed system — a message queue, consensus protocol, or leader election — either solo or with others in breakout rooms.
• 💬 Open Discussion
  How formal modeling can help surface design flaws early, and what makes a good specification approachable.

Why attend:
This is a friendly, interactive online session for anyone curious about formal modeling or distributed systems. No prior experience required — just bring curiosity and a willingness to think rigorously about correctness.