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. Alloy aporta una herramienta de modelaje estructural sencilla basada en lógica de primer orden. 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. Las especificaciones de Alloy pueden ser comprobadas empleando el Analizador de Alloy.

La primera version del lenguaje Alloy apareció en 1997. Era más bien un limitado lenguaje de modelado de objetos. Las sucesivas iteraciones del lenguaje "añadieron cuantificadores, mayores relaciones de aridad, polimorfismo, composición y firmas".^[2]​ Aunque Alloy está diseñado con un análisis automático en mente, Alloy difiere de muchos lenguajes de especificación por la comprobación de modelo en la que permite la definición de modelos infinitos. El analizador de Alloy está diseñado para realizar comprobaciones de alcance finito incluso en modelos infinitos.

Los modelos de Alloy son naturalmente relacionales, y están compuesto de vastos tipos diferentes de estamentos:^[1]​

• Firmas. Definen el vocabulario del modelo creando nuevos conjuntos.
• Hechos. Son <<constraints>> que se asume siempre conservarán.
• Predicados. Son <<constraints>> parametrizados, y pueden ser empleados para representar operaciones.
• Funciones. Son expresiones que devuelven resultados.
• Aserciones. Son conjeturas sobre el modelo que pueden ser verificadas asando el analizador de Alloy.

Ya que Alloy es un lenguaje declarativo el significado de un modelo no se ve afectado por el orden de los estamentos.