Version 4 of the Alloy Analyzer is a complete rewrite, offering improvements in robustness, performance and usability. The new codebase is approximately a quarter of the size of the codebase of Alloy 3. Compilation is now instantaneous for all but the largest models, and analysis is often a factor of 2-10 faster. We recommend that all users switch to this new version. There are a small number of syntactic improvements over Alloy 3, and models written in Alloy 3 will therefore require some very small alterations to run in Alloy 4.

The Alloy Analyzer 4 is based on the new SAT-based model finder Kodkod. Kodkod applies new techniques and optimizations to the translation from relational to boolean logic, such as user-provided partial instances and a more general symmetry-breaking technique that works in the presence of arbitrary partial instances.

Download the Alloy Analyzer and related documentation here.