Alloy is a language for describing 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. Hundreds of projects have used Alloy for design analysis, for verification, for simulation, and as a backend for many other kinds of analysis and synthesis tools, and Alloy is currently being taught in courses worldwide.

The official Alloy website provides links to downloads, tutorials and case studies.

A recent CACM paper gives an overview of Alloy and its applications to date, and is accompanied by a video showing Alloy in action.

Some recent applications include: exploiting Spectre/Meltdown, game design, memory models, peer-to-peer, storm surge protection, radiotherapy.