Did you already watch the linked video (https://news.ycombinator.com/item?id=35512991 https://news.ycombinator.com/item?id=35512991) and go through Alloy's tuto

Did you already watch the linked video (https://news.ycombinator.com/item?id=35512991 https://news.ycombinator.com/item?id=35512991) and go through Alloy's tutorial? https://alloytools.org/tutorials/online/ https://alloytools.org/tutorials/online/ Based on the approach taken by the presenter from the video, I'd guess the "hands on" you're looking for is to take some API that you serve to others, internally or externally, and start writing down things you believe are invariant about it. Inputs must have a length greater than 1? Well, do all downstream systems also honor that invariant?