I thought about trying Alloy since in not mathematical enough for HOL, etc. An EAL7 VPN project used it too, IIRC. Do you have a link to a tutorial or reference for how you apply it to data structure def's?
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.
Another interesting tool is ProB[1]. I believe it does symbolic model checking and supports partial order reduction. It works on specifications in multiple languages, including TLA+, but I haven't had the chance to use it myself because it doesn't support all TLA+ features. In particular, it doesn't support TLA+'s higher-order operators, which my specifications use.
Appreciate the reference. I'm holding off on ProB and B for now because the B method has mixed results in CompSci literature. I mean, it's been proven on a number of high assurance projects by pro's. I at least like that both B and TLA+ are pretty straight-forward to compared to most where a person has both a mathematical and good, mental model of what's going on. B particularly as it maps to imperative with ease.
I'm keeping it bookmarked just in case. Meanwhile, I just got a ton of stuff on asynchronous verification in response to another commenter's troubles there. I was away too long: looks like async and GALS are both mostly solved problems at the cutting edge with some tools to help. A lot to skim or read that puts my B experiments further on the backlog.
