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.