Alloy 4 is a self-contained executable, which includes the Kodkod model finder and a variety of SAT solvers, as well as the standard Alloy library and a collection of tutorial examples. The same jar file can be incorporated into other applications to use Alloy as an API, and includes the source code.

To execute, simply double-click on the jar file, or type java -jar alloy4.jar in a console.

FAQ Frequently asked questions about Alloy
reference Download language reference for Alloy 4 (PDF)
comparisons Comparisons to Z, B, VDM and OCL (PDF)
grammar A grammar for Alloy 4 in plain text (TXT), also see the cup file
quick guide Overview of new features in Alloy 4
Alloy API Documentation for Alloy API
Alloy API Examples examples of using the compiler, the ast, the evaluator
online tutorial A step-by-step walkthrough and tutorial for Alloy 4
tutorial slides Slides for day-long tutorial by Rob Seater and Greg Dennis
digital humanities tutorial A tutorial introducing Alloy for digital humanities work, by C. M. Sperberg-McQueen