I just had a quick look at Alloy ([0]), and I'm interested in how it could be integrated into the software development process -- once you're confident about your Alloy model, you have to transfer it to working code somehow. I'd try to use both "fact" and "assert" statements from Alloy code as assertions in my production code (e.g. Python or Java). How is this usually done?

[0] http://www.doc.ic.ac.uk/project/examples/2007/271j/suprema_o...