A Guide to Alloy
An Introduction To Alloy

Software development is difficult; choosing correct abstractions to base your design around is a tricky process! Quite often apparently simple and robust designs can turn out to be incoherent and even inconsistent when you come to implement them.

One way to avoid this problem of "wishful thinking" as well as making software development more straightforward is through formal specification. This method approaches software abstraction head-on using precise and unambiguous notation, one such example is the declarative language Z.

Naturally this is not fool proof either though; proving your specification is correct/sound requires a substantial amount of effort. Whilst conventional theorem based analysis tools have improved, their level of automation is still relatively poor compared to model checkers.

Hence, Alloy was developed in the hope of adapting a declarative language like Z to bring in fully automatic analysis. To do this Alloy sacrifices the ability to totally prove a system's correctness. Rather, it attempts to find counterexamples within a limited scope that violate the constraints of the system. Thus by combining the best of both worlds Alloy produces a rigorous model that gives the user immediate feedback
Main Developer
Professor Daniel Jackson


The design was done by the Software Design Group at MIT lead by Professor Daniel Jackson. In 1997 they produced the first Alloy prototype, which was then a rather limited object modelling language. Over the years Alloy has developed into a full structural modelling language capable of expressing complex structural constraints and behaviour.

By employing first order logic, Alloy is able to translate specifications into large Boolean expression that can be automatically analyzed by SAT solvers. Thus when given a logical formula (in Alloy), the Alloy Analyzer can attempt to find a model which satisfies it.

One of the great benefits this lends to Alloy is the ability of incremental analysis. A programmer may explore design ideas starting from a tiny model which is then scaled up, with Alloy able to analyse it at every step.

Alloy has gradually improved in performance and scalability and been applied to many fields including scheduling, cryptography and instant messaging.


For more information on Alloy, we recommend the following:


You can download the Alloy Analyzer from the following sources: