[maramono]

I've used it several times but the big problem with it is that once you have a nice, correct model that has been checked (and no counterexamples found), there's no way to translate it to code. This meand that your basically back on square one in terms of implementation.

I really like (and use quite often) the ASM method instead.

More of my thoughts here: http://ortask.com/how-i-designed-built-and-tested-a-temperat...

[nickpsecurity]

There's actually been imperative extensions and prolog compilers for it. Here you go:

https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf

Also, for ASM's, the most interesting one I've seen is certified compiler project that is taking a lot less lines of code than CompCert:

https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf