I was exposed to alloy by this wonderful video:

"Finding bugs without running or even looking at code" by Jay Parlar

https://www.youtube.com/watch?v=FvNRlE4E9QQ

I believe the general idea could be applicable in practice for core parts of most businesses software. So now I'm very interested in real world accounts of using alloy like this.

Anyone have other posts like this one or experiences to share along these lines?