Alloy is used in a wide variety of applications. The page provides links to some tools built on Alloy and Kodkod (Alloy’s model finding engine), and to lists of citations from Google Scholar of papers that discuss applications of Alloy.

alloy citations

Google scholar	A sample of over 1200 papers discussing Alloy
case studies	Selected papers describing applications of Alloy
courses	Courses using Alloy
translations	Papers on translating a dozen other languages into Alloy
theses	Theses about Alloy

select tools built on alloy and kodkod

Alloy*	A general-purpose, higher-order, relational constraint solver
aRby	An embedding of Alloy in Ruby
Forge	A bounded verifier for Java code
Squander	Unified execution of imperative and declarative code
Alloy4Eclipse	Eclipse plugin for Alloy 4
DynAlloy	An extension of Alloy with procedural actions
TACO	A bounded verifier for Java annotated with JML
Equals Checker	A tool for checking equals methods in Java
Nitpick	A counterexample generator for Isabelle/HOL
Margrave	A security policy analyzer for firewalls
Secrecy Modeling Language (SML)	A language for composing and validating security models.
Lightning	An Eclipse plugin allowing to specify graphical DSLs in Alloy
Echo	A tool for model repair and transformation built over Alloy