En ciencia de los computadores e ingeniería informática, Alloy es un lenguaje de especificación declarativo para expresar complejas estructuras de control y comportamiento en un sistema software.
Los soportes matemáticos del lenguaje fueron fuertemente influenciados por la notación Z, aunque la sintaxis de Alloy debe más a lenguajes tales como el lenguaje de control de objetos.
[1] Alloy está orientado a la creación de micro-modelos que pueden ser automáticamente comprobados para su correctitud.
La primera version del lenguaje Alloy apareció en 1997.
Las sucesivas iteraciones del lenguaje "añadieron cuantificadores, mayores relaciones de aridad, polimorfismo, composición y firmas".