Alloy is a language for describing evolving structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.

An Alloy model is a collection of constraints that describes (implicitly) a set of structures that may evolve along time, for example: all the possible security configurations of a web application, or all the possible topologies of a switching network. Alloy’s tool, the Alloy Analyzer, is a solver that takes the constraints of a model and finds structures that satisfy them. It can be used both to explore the model by generating sample structures, and to check properties of the model by generating counterexamples. Structures are displayed graphically, and their appearance can be customized for the domain at hand.

At its core, the Alloy language is a simple but expressive logic based on the notion of relations, and was inspired by the Z specification language, Tarski’s relational calculus and the Linear Temporal Logic with Past. Alloy’s syntax is designed to make it easy to build models incrementally, and was influenced by modeling languages (such as the object models of OMT and UML). Novel features of Alloy includes many new rich subtype facilities for factoring out common features and a uniform and powerful syntax for navigation expressions.

Alloy was created in the Software Design Group at MIT.

current alloy team members

former team members

Major contributions to earlier versions of Alloy were made by: Emina Torlak, Eunsuk Kang, Joe Near, Felix Chang, Jonathan Edwards, Robert Seater, Derek Rayside, Greg Dennis, Ilya Shlyakhter, Mana Taghdiri, Mandana Vaziri, Sarfraz Khurshid, Manu Sridharan, and Denis Kuperberg.

alloy board

The future of Alloy is monitored by the Alloy Board, composed of:

  • Daniel Jackson
  • Tim Nelson
  • Peter Kriens
  • Aleksandar Milicevic
  • Emina Torlak
  • Cesare Tinelli
  • Sarfraz Khurshid
  • Pamela Zave
  • Eunsuk Kang
  • Hillel Wayne
  • Alcino Cunha
  • David Chemouil
  • Derek Rayside
  • John Baugh
  • Julien Brunel
  • Matthew Di Ferrante
  • Nuno Macedo

acknowledgements

Alloy is the product of a research project funded by the National Science Foundation under Grant Nos. 0325283, 0541183, 0438897 and 0707612; by the Air Force Research Laboratory (AFRL/IF) and the Disruptive Technology Office (DTO) in the National Intelligence Community Information Assurance Research (NICIAR) Program; and by the Nokia Corporation as part of a collaboration between Nokia Research and MIT CSAIL. Alloy 6 was funded by the European Regional Development Fund (ERDF) via Operational Programme for Competitiveness and Internationalisation (COMPETE 2020) ; Fundação para a Ciência e a Tecnologia (FCT) projet POCI-01-0145-FEDER-016826; French projects DGA/ANR Cx (ANR-13-ASTR-0006) and ANR FORMEDICIS (ANR-16-CE25-0007).