I use the visualizer and just worked through the examples and tutorials on the Alloy website. It takes a little bit to get used to, but the visualizations reall

I use the visualizer and just worked through the examples and tutorials on the Alloy website. It takes a little bit to get used to, but the visualizations really help to see what's going on. What I like Alloy for is checking to see if the operations you're defining to maintain a data structure actually maintain the desired invariants. It's nice for situations where you're not actually sure that what you're "trying to do" will even work like you expect. With Coq, I tend to already know something will work and just want to verify that I've achieved it, so it's much less exploratory in nature.