Alloy (specification language)

The Alloy language and analyzer are developed by a team led by Daniel Jackson at the Massachusetts Institute of Technology in the United States.

Succeeding iterations of the language "added quantifiers, higher arity relations, polymorphism, subtyping, and signatures".

As such, it is intended to provide fully automated analysis, in contrast to the interactive theorem proving techniques commonly used with specification languages similar to Alloy.

However, model-checking is ill-suited to the kind of models that are typically developed in Alloy, and as a result the core of the Analyzer was eventually implemented as a model-finder built atop a boolean SAT solver.

In the event that the solver finds a solution, the result is translated back into a corresponding binding of constants to variables in the relational logic model.