Can you precisely describe what a "correct state" of your system is? If so, you have an inductive invariant. That means your system is less likely to do bad things AND you're closer to proving it. We wrote a guide on how to get there ⬇️

Defining "correct state" is surprisingly hard. Quint's newest feature makes it approachable with interactive feedback that teaches you what you missed.

In today's blog, we show the step-by-step process with reliable broadcast, starting general and letting Quint refine our thinking until we got it right. Learn how: