The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

We have just released Alloy 3.0-Beta and will soon be releasing a stable version. We'd like to hear from you! Please send bug reports, questions, and requests to
Downloads - analyzer distribution, reference manual, miscellaneous tools
New in v3.0 - how Alloy 3.0 differs from Alloy 2.0
Quick Start - brief overview of using Alloy to analyze models
Online Tutorial - introduction to Alloy and advice on writing models. PDF version: (zip) (tar).
FAQ - frequently asked questions, Alloy's history and philosophy
Publications - papers and theses on Alloy
Talks - talks about Alloy
Courses - Alloy as a teaching tool
Case Studies - case studies using Alloy
Alloy-Discuss - Yahoo discussion group

To receive emails about Alloy updates and releases, add yourself to the alloy announce email list.