> ## Documentation Index
> Fetch the complete documentation index at: https://docs.alchemicalchef.io/llms.txt
> Use this file to discover all available pages before exploring further.

# Alloy Syntax Guide

> Comprehensive reference for Alloy syntax, operators, and patterns. Everything you need to write production specifications.

This guide covers Alloy syntax comprehensively. If you're new to Alloy, start with [Alloy Basics](/formal-methods/alloy-basics) for a gentler introduction. This reference assumes you understand the core concepts: signatures, relations, facts, and the basic workflow.

Alloy 6 introduced temporal operators for modeling state over time. This guide covers both classic (static) Alloy and the temporal extensions.

## When to Use Alloy

Alloy excels at finding counterexamples to structural properties. Use it when you need to answer:

* "Can this bad state exist?" - Alloy searches for violations
* "Is this constraint sufficient?" - Alloy finds gaps
* "What does this data model actually allow?" - Alloy generates instances

Alloy uses SAT-based bounded verification. It doesn't prove properties hold for all possible sizes, it exhaustively checks within the bounds you specify (typically 3-5 atoms per signature). This is usually enough to find bugs; most flaws manifest in small counterexamples.

For temporal properties like "this eventually happens" or protocol correctness over time, consider [TLA+](/formal-methods/tla-basics).

The two tools complement each other well.

## Signatures

Signatures define the types of atoms in your model. They're like classes in OOP or tables in a database, but with relational semantics.

### Basic Signatures

```alloy theme={null}
sig Person {}           -- A set of Person atoms
sig File {}             -- A set of File atoms
sig Empty {}            -- Can be empty (zero atoms)
```

### Signature Modifiers

```alloy theme={null}
one sig Root {}           -- Exactly one atom
lone sig Config {}        -- Zero or one atom
some sig Node {}          -- At least one atom
abstract sig Entity {}    -- No direct atoms (only via extensions)
```

The `one`, `lone`, and `some` modifiers constrain cardinality:

| Modifier   | Meaning       | Atoms             |
| ---------- | ------------- | ----------------- |
| (none)     | Any number    | 0, 1, 2, ...      |
| `one`      | Exactly one   | 1                 |
| `lone`     | At most one   | 0 or 1            |
| `some`     | At least one  | 1, 2, 3, ...      |
| `abstract` | None directly | 0 (only subtypes) |

### Signature Extension

```alloy theme={null}
abstract sig Animal {}
sig Cat extends Animal {}
sig Dog extends Animal {}
```

Extensions create subtypes. Each Cat atom is also an Animal atom. Extensions are unique in the sense that no atom is both a Cat and a Dog.

### Signature Subsets

```alloy theme={null}
sig Person {}
sig Employee in Person {}
sig Manager in Employee {}
```

The `in` keyword creates subsets that aren't necessarily unique. An atom can be both an Employee and something else that extends Person.

### Disjoint Subsets

```alloy theme={null}
sig Person {}
sig Student, Faculty in Person {}
-- Student and Faculty can overlap (a Person can be both)

-- To make them disjoint, add a fact:
fact { no Student & Faculty }
-- Or use disj in quantifiers:
-- all disj s: Student, f: Faculty | ...
```

To ensure subsets don't overlap, add a disjointness fact. A Person can still be neither Student nor Faculty.

## Fields and Multiplicity

Fields define relations between signatures. Every field is a relation, even "attributes" are relations to value atoms.

### Field Multiplicity

```alloy theme={null}
sig Person {
    name: one String,        -- Exactly one name (required)
    spouse: lone Person,     -- Zero or one spouse (optional)
    children: set Person,    -- Zero or more children
    parents: some Person     -- One or more parents (at least one)
}
```

| Keyword | Meaning      | Count |
| ------- | ------------ | ----- |
| `one`   | Exactly one  | 1     |
| `lone`  | At most one  | 0-1   |
| `set`   | Any number   | 0+    |
| `some`  | At least one | 1+    |

Without a keyword, `one` is assumed for simple relations. For relations with arrow (`->`), `set` is the default.

### Binary Relations

Most fields are binary relations (from this signature to another):

```alloy theme={null}
sig File {
    parent: one Folder,      -- File -> Folder
    owner: one User          -- File -> User
}
```

### Ternary and Higher Relations

Relations can have higher arity:

```alloy theme={null}
sig Person {
    -- For each Person, maps Organizations to Roles
    membership: Organization -> Role
}

sig Object {
    -- Access control: Subject -> Permission mapping
    access: Subject -> Permission
}
```

To use: `p.membership[org]` returns the roles person `p` has in organization `org`.

### Relation Constraints

```alloy theme={null}
sig Node {
    edges: set Node
}

-- Self-loops allowed by default; prevent with fact:
fact NoSelfLoops {
    no n: Node | n in n.edges
}

-- Symmetric relation (bidirectional edges):
fact Symmetric {
    all n1, n2: Node | n1 in n2.edges implies n2 in n1.edges
}
```

## Relational Operators

Alloy is fundamentally relational. Understanding these operators is essential.

### Join (.)

The dot operator navigates relations:

```alloy theme={null}
sig Person {
    father: lone Person,
    mother: lone Person
}

p.father          -- p's father (a Person or empty)
p.father.father   -- p's paternal grandfather
p.(father + mother)  -- p's father or mother
```

Join composes relations. If `r: A -> B` and `s: B -> C`, then `r.s: A -> C`.

### Union (+)

Combines sets or relations:

```alloy theme={null}
Cat + Dog                    -- All cats and dogs
p.father + p.mother          -- p's parents
read + write                 -- Union of permissions
```

### Intersection (&)

Elements in both:

```alloy theme={null}
Employee & Manager           -- People who are both
trusted & external           -- Trusted external entities
```

### Difference (-)

Elements in first but not second:

```alloy theme={null}
Person - Employee            -- Non-employees
all - allowed                -- Forbidden items
```

### Transpose (\~)

Reverses a relation:

```alloy theme={null}
sig File {
    parent: one Folder
}

~parent                      -- Folder -> File (children)
f.~parent                    -- Files in folder f
```

If `r: A -> B`, then `~r: B -> A`.

### Transitive Closure (^)

One or more applications of a relation:

```alloy theme={null}
sig Folder {
    parent: lone Folder
}

f.^parent                    -- All ancestors of f
^parent                      -- The ancestor relation
n in n.^parent               -- n is its own ancestor (cycle!)
```

Transitive closure is powerful for reachability, ancestry, and graph analysis.

### Reflexive Transitive Closure (\*)

Zero or more applications (includes identity):

```alloy theme={null}
f.*parent                    -- f and all its ancestors
*parent                      -- The "ancestor or self" relation
```

The difference: `^r` requires at least one step; `*r` includes staying in place.

### Product (->)

Creates pairs:

```alloy theme={null}
User -> File                 -- All user-file pairs
alice -> secret              -- Specific pair
Person -> Person -> Action   -- Ternary relation
```

### Domain Restriction (`<:`)

Limits a relation to a domain subset:

```alloy theme={null}
Employee <: salary           -- salary restricted to Employees
trusted <: access            -- access for trusted entities only
```

If `r: A -> B` and `s: set A`, then `s <: r: A -> B` contains only pairs where the first element is in `s`.

### Range Restriction (`:>`)

Limits a relation to a range subset:

```alloy theme={null}
knows :> Employee            -- knowing relationships to Employees
access :> ReadOnly           -- access limited to read-only perms
```

If `r: A -> B` and `s: set B`, then `r :> s: A -> B` contains only pairs where the second element is in `s`.

### Override (++)

Replaces mappings:

```alloy theme={null}
defaults ++ customSettings   -- custom overrides defaults
oldState ++ (key -> newValue)  -- Update specific mapping
```

For function-like relations, `++` updates entries. If `key` exists in `oldState`, the new value replaces it.

### Cardinality (#)

Counts elements:

```alloy theme={null}
#Person                      -- Number of persons
#(p.friends)                 -- Number of p's friends
#File > 0                    -- At least one file exists
```

## Quantifiers

Quantifiers express properties over sets.

### Universal (all)

```alloy theme={null}
all p: Person | p.age >= 0
all f: File | one f.parent
all x, y: Node | x.edge = y implies y.edge = x
```

Every element satisfies the condition.

### Existential (some)

```alloy theme={null}
some p: Person | p.age > 100
some f: File | no f.parent
some x, y: Node | x != y and x in y.edge
```

At least one element satisfies the condition.

### None (no)

```alloy theme={null}
no p: Person | p.age < 0
no f: Folder | f in f.^parent
no disj x, y: Node | x.edge = y.edge
```

No element satisfies the condition. Equivalent to `not some`.

### Unique (one)

```alloy theme={null}
one p: Person | p.name = "Alice"
one f: File | f.size = max[File.size]
```

Exactly one element satisfies the condition.

### At Most One (lone)

```alloy theme={null}
lone p: Person | p.role = CEO
lone f: File | no f.parent
```

Zero or one element satisfies the condition.

### Disjoint Quantification

```alloy theme={null}
all disj x, y: Person | x.id != y.id
some disj a, b, c: Node | a->b + b->c in edge
```

The `disj` modifier ensures quantified variables are distinct.

### Logical Operators

Combine quantified expressions:

```alloy theme={null}
-- Conjunction
all p: Person | p.age >= 0 and p.age <= 150

-- Disjunction
all f: File | f.public or some f.owner

-- Implication
all p: Person | p.employed implies some p.salary

-- Biconditional
all x: Node | x.root iff no x.parent

-- Negation
all p: Person | not p in p.^parent
```

| Operator         | Meaning           |
| ---------------- | ----------------- |
| `and`            | Both true         |
| `or`             | At least one true |
| `implies` / `=>` | If-then           |
| `iff` / `<=>`    | If and only if    |
| `not` / `!`      | Negation          |

## Facts, Predicates, Functions, Assertions

These organize constraints and queries.

### Facts

Facts are constraints that *always* hold. Alloy only considers instances satisfying all facts.

```alloy theme={null}
fact NoSelfEmployment {
    no p: Person | p in p.manages
}

fact AcyclicHierarchy {
    all p: Person | p not in p.^manages
}

-- Anonymous fact (no name)
fact {
    all f: File | some f.owner
}
```

Facts constrain the search space. Use them for invariants that define your model.

### Predicates

Predicates are named, parameterized formulas. They can be true or false.

```alloy theme={null}
pred isManager[p: Person] {
    some p.manages
}

pred canAccess[u: User, f: File] {
    f in u.owns or f in u.sharedWith
}

pred wellFormed {
    all f: File | some f.parent
    no f: Folder | f in f.^parent
}
```

Use predicates to define reusable conditions or as targets for `run` commands.

### Functions

Functions return values (sets/relations). They're expressions, not constraints.

```alloy theme={null}
fun parents[p: Person]: set Person {
    p.father + p.mother
}

fun ancestors[p: Person]: set Person {
    p.^(father + mother)
}

fun commonFriends[p1, p2: Person]: set Person {
    p1.friends & p2.friends
}

-- Functions can return relations
fun familyRelation: Person -> Person {
    father + mother + ~father + ~mother
}
```

### Assertions

Assertions are properties you claim should hold. The `check` command searches for violations.

```alloy theme={null}
assert NoOrphans {
    all f: File | some f.parent or f in RootFolder
}

assert TransitiveClosure {
    all p: Person | p.ancestor = p.^parent
}

assert PermissionConsistency {
    all u: User, f: File |
        canRead[u, f] implies canAccess[u, f]
}
```

Unlike facts, assertions don't constrain the model, they query it.

## Comprehensions

Set comprehensions build sets from expressions.

### Basic Comprehension

```alloy theme={null}
{ p: Person | p.age > 21 }           -- Adults
{ f: File | no f.owner }             -- Unowned files
{ x: Node | x in x.^next }           -- Nodes in cycles
```

### Expression Comprehension

```alloy theme={null}
{ p: Person, f: File | f in p.owns } -- Ownership pairs
{ x, y: Node | x->y in edges }       -- Edge pairs
```

### In Predicates and Functions

```alloy theme={null}
fun adults: set Person {
    { p: Person | p.age >= 18 }
}

pred allFilesOwned {
    no { f: File | no f.owner }
}
```

## Let Expressions

`let` binds names to expressions for clarity and reuse.

```alloy theme={null}
pred complexCondition[p: Person] {
    let parents = p.father + p.mother,
        siblings = parents.~(father + mother) - p |
    some siblings and #parents = 2
}

fun reachable[start: Node]: set Node {
    let direct = start.edges,
        indirect = direct.^edges |
    direct + indirect
}
```

Let bindings are purely syntactic, they don't affect semantics.

## Commands

Commands tell the Analyzer what to do.

### Run

The `run` command searches for instances.

```alloy theme={null}
run {}                           -- Any valid instance
run { some File }                -- Instance with files
run wellFormed                   -- Instance where predicate holds
run { #Person = 3 }              -- Exactly 3 persons
```

### Check

The `check` command searches for assertion violations.

```alloy theme={null}
check NoOrphans                  -- Find counterexample
check PermissionConsistency      -- Verify property
check { all f: File | some f.owner }  -- Inline assertion
```

### Scope

Bounds limit the search space. By default, bounds mean "at most N atoms" (0 to N), not "exactly N."

```alloy theme={null}
run {} for 5                     -- 0 to 5 of each signature
run {} for 3 File, 2 Folder      -- 0-3 Files, 0-2 Folders
run {} for exactly 3 Person      -- Exactly 3 (not 0 to 3)
run {} for 5 but 2 Int           -- 5 default, but 2-bit integers (-2 to 1)
```

```alloy theme={null}
check NoOrphans for 10           -- Check with 0-10 atoms per signature
check NoOrphans for 3 but 5 File -- 0-3 default, 0-5 files
```

Use `exactly` when you need a specific count. Without it, Alloy explores all sizes up to the bound, which is usually what you want for finding counterexamples.

### Expect

Expect indicates anticipated results (for documentation/testing).

```alloy theme={null}
run {} for 3 expect 1            -- Expect satisfiable
check NoOrphans expect 0         -- Expect no counterexample
```

## Module System

Modules organize specifications into reusable units.

### Basic Modules

```alloy theme={null}
module filesystem

sig File { ... }
sig Folder { ... }
```

### Opening Modules

```alloy theme={null}
module main

open filesystem                  -- Import all from filesystem
open util/ordering[Time]         -- Parameterized utility module
open util/relation               -- Relation utilities
```

### Private Declarations

```alloy theme={null}
module internal

private sig Helper {}            -- Not visible when opened
sig Public {}                    -- Visible
```

### Parameterized Modules

```alloy theme={null}
module graph[Node]

sig Edge {
    src, dst: one Node
}

pred connected[n1, n2: Node] {
    n2 in n1.^(~src.dst)
}
```

Usage:

```alloy theme={null}
open graph[Computer]             -- Instantiate with Computer
```

### Standard Library

Alloy includes utility modules:

```alloy theme={null}
open util/ordering[State]        -- Total ordering on State
open util/relation               -- Relation predicates
open util/ternary                -- Ternary relation utilities
open util/boolean                -- Boolean operations
open util/integer                -- Integer operations
open util/sequence[Elem]         -- Sequences
```

## Temporal Operators (Alloy 6)

Alloy 6 introduced temporal logic for modeling state over time.

### Variable Fields

```alloy theme={null}
sig Buffer {
    var contents: set Data,      -- Changes over time
    capacity: one Int            -- Static (no var)
}
```

The `var` keyword marks mutable relations.

### Priming

The prime operator (`'`) refers to the next state:

```alloy theme={null}
pred addData[b: Buffer, d: Data] {
    d not in b.contents          -- Precondition
    b.contents' = b.contents + d -- Postcondition
}
```

### Temporal Quantifiers

```alloy theme={null}
-- Future-time operators
always P                         -- P holds in every future state
eventually P                     -- P holds in some future state
after P                          -- P holds in the next state
P until Q                        -- P holds until Q becomes true
P releases Q                     -- Q holds until P becomes true (or forever)

-- Past-time operators
historically P                   -- P held in all past states
once P                           -- P held at some past state
before P                         -- P held in the previous state
P since Q                        -- P has held since Q was true
```

### Traces and Liveness

```alloy theme={null}
-- Specification: initial state + transitions
fact Traces {
    init
    always trans
}

pred init {
    no Buffer.contents
}

pred trans {
    some b: Buffer, d: Data | addData[b, d]
    or stutter
}

pred stutter {
    contents' = contents
}

-- Liveness: something eventually happens
assert EventuallyFull {
    always (some b: Buffer | eventually #b.contents = b.capacity)
}
```

### Temporal Example: Mutex

```alloy theme={null}
module mutex

abstract sig Process {
    var state: one State
}

abstract sig State {}
one sig Idle, Waiting, Critical extends State {}

one sig P1, P2 extends Process {}

pred init {
    all p: Process | p.state = Idle
}

pred requestAccess[p: Process] {
    p.state = Idle
    p.state' = Waiting
    all other: Process - p | other.state' = other.state
}

pred enterCritical[p: Process] {
    p.state = Waiting
    no other: Process - p | other.state = Critical
    p.state' = Critical
    all other: Process - p | other.state' = other.state
}

pred exitCritical[p: Process] {
    p.state = Critical
    p.state' = Idle
    all other: Process - p | other.state' = other.state
}

pred stutter {
    all p: Process | p.state' = p.state
}

pred trans {
    (some p: Process | requestAccess[p] or enterCritical[p] or exitCritical[p])
    or stutter
}

fact Traces {
    init
    always trans
}

-- Safety: mutual exclusion
assert MutualExclusion {
    always (lone p: Process | p.state = Critical)
}

-- Liveness: no starvation (if waiting, eventually critical)
-- Note: This will fail without fairness constraints - one process can
-- repeatedly enter/exit while another waits forever
assert NoStarvation {
    all p: Process | always (p.state = Waiting implies eventually p.state = Critical)
}

check MutualExclusion for 5 steps
check NoStarvation for 10 steps
```

## Built-in Relations and Constants

### Universal Set

```alloy theme={null}
univ                             -- All atoms
Person in univ                   -- Always true
univ - Person                    -- All non-Person atoms
```

### Empty Set

```alloy theme={null}
none                             -- Empty set
no x implies x = none            -- Equivalence
```

### Identity Relation

```alloy theme={null}
iden                             -- Identity: x->x for all x
r & iden                         -- Self-loops in r
r - iden                         -- Remove self-loops
```

### Integer Operations

```alloy theme={null}
-- Arithmetic
plus[x, y]                       -- x + y
minus[x, y]                      -- x - y
mul[x, y]                        -- x * y
div[x, y]                        -- x / y
rem[x, y]                        -- x % y

-- Comparison
x < y, x > y, x <= y, x >= y

-- Aggregation
sum[s]                           -- Sum of integer set
max[s], min[s]                   -- Maximum/minimum

-- Integer set
Int                              -- All integers in scope
```

Note: Alloy uses bounded integers. The default is 4-bit, giving a range of -8 to 7. Use `for N Int` to set bitwidth (e.g., `for 5 Int` gives 5-bit integers: -16 to 15). Integer overflow wraps silently, so increase bitwidth if your model uses larger numbers.

## Common Patterns

### State Machine

```alloy theme={null}
abstract sig State {}
one sig S1, S2, S3 extends State {}

sig Machine {
    var current: one State
}

pred transition[m: Machine, from, to: State] {
    m.current = from
    m.current' = to
}
```

### Graph Reachability

```alloy theme={null}
sig Node {
    edges: set Node
}

fun reachable[n: Node]: set Node {
    n.*edges
}

pred connected {
    all n1, n2: Node | n2 in reachable[n1]
}

pred acyclic {
    no n: Node | n in n.^edges
}
```

### Ownership / Containment

```alloy theme={null}
sig Container {
    contains: set Item
}

sig Item {
    inside: lone Container
}

fact Consistency {
    all c: Container, i: Item |
        i in c.contains iff i.inside = c
}

fact SingleOwner {
    all i: Item | lone i.inside
}
```

### Access Control

```alloy theme={null}
sig Subject {}
sig Object {}
sig Permission {}

sig AccessMatrix {
    access: Subject -> Object -> Permission
}

pred canAccess[s: Subject, o: Object, p: Permission] {
    some am: AccessMatrix | p in am.access[s][o]
}
```

### Ordered Elements

```alloy theme={null}
open util/ordering[Time]

sig Time {}

sig Event {
    when: one Time
}

pred before[e1, e2: Event] {
    lt[e1.when, e2.when]
}

fact EventOrder {
    all e1, e2: Event | e1 != e2 implies
        (before[e1, e2] or before[e2, e1])
}
```

## Complete Example: Key-Value Store

A specification combining multiple concepts:

```alloy theme={null}
module kvstore

sig Key {}
sig Value {}

sig Store {
    var data: Key -> lone Value
}

one sig TheStore extends Store {}

pred init {
    no TheStore.data
}

pred put[k: Key, v: Value] {
    TheStore.data' = TheStore.data ++ (k -> v)
}

pred get[k: Key, v: Value] {
    v = TheStore.data[k]
    TheStore.data' = TheStore.data  -- Frame condition
}

pred delete[k: Key] {
    TheStore.data' = TheStore.data - (k -> Value)
}

pred trans {
    (some k: Key, v: Value | put[k, v])
    or (some k: Key | delete[k])
    or (TheStore.data' = TheStore.data)  -- Stutter
}

fact Traces {
    init
    always trans
}

-- Each key maps to at most one value
assert Functional {
    always all k: Key | lone TheStore.data[k]
}

-- If we put k->v and don't delete or overwrite, it stays
assert PutPersists {
    all k: Key, v: Value |
        always (put[k, v] and after always (not delete[k] and not (some v': Value - v | put[k, v'])))
            implies after always TheStore.data[k] = v
}

-- Delete removes the key
assert DeleteRemoves {
    all k: Key |
        always (delete[k] implies after no TheStore.data[k])
}

check Functional for 3 but 5 steps
check PutPersists for 3 but 8 steps
check DeleteRemoves for 3 but 5 steps

run { eventually some TheStore.data } for 3 but 5 steps
```

## Quick Reference

### Signature Modifiers

| Modifier   | Meaning                       |
| ---------- | ----------------------------- |
| `one`      | Exactly one atom              |
| `lone`     | Zero or one atom              |
| `some`     | At least one atom             |
| `abstract` | No direct atoms               |
| `extends`  | Disjoint subtype              |
| `in`       | Subset (possibly overlapping) |

### Field Multiplicity

| Keyword | Meaning                |
| ------- | ---------------------- |
| `one`   | Exactly one            |
| `lone`  | Zero or one            |
| `some`  | One or more            |
| `set`   | Zero or more (default) |

### Relational Operators

| Operator | Name                         | Purpose            |
| -------- | ---------------------------- | ------------------ |
| `.`      | Join                         | Navigate relations |
| `+`      | Union                        | Combine sets       |
| `&`      | Intersection                 | Common elements    |
| `-`      | Difference                   | Remove elements    |
| `~`      | Transpose                    | Reverse relation   |
| `^`      | Transitive closure           | One+ steps         |
| `*`      | Reflexive transitive closure | Zero+ steps        |
| `->`     | Product                      | Create tuples      |
| `<:`     | Domain restriction           | Filter by domain   |
| `:>`     | Range restriction            | Filter by range    |
| `++`     | Override                     | Replace mappings   |
| `#`      | Cardinality                  | Count elements     |

### Logical Operators

| Operator         | Meaning       |
| ---------------- | ------------- |
| `and`            | Conjunction   |
| `or`             | Disjunction   |
| `not` / `!`      | Negation      |
| `implies` / `=>` | Implication   |
| `iff` / `<=>`    | Biconditional |

### Quantifiers

| Quantifier | Meaning      |
| ---------- | ------------ |
| `all`      | For every    |
| `some`     | There exists |
| `no`       | For none     |
| `one`      | Exactly one  |
| `lone`     | At most one  |

### Temporal Operators (Alloy 6)

| Operator       | Meaning                      |
| -------------- | ---------------------------- |
| `'`            | Next state value             |
| `always`       | In all future states         |
| `eventually`   | In some future state         |
| `after`        | In the next state            |
| `until`        | P holds until Q              |
| `releases`     | Q holds until P (or forever) |
| `historically` | In all past states           |
| `once`         | In some past state           |
| `before`       | In the previous state        |
| `since`        | P has held since Q           |

### Commands

| Command         | Purpose                            |
| --------------- | ---------------------------------- |
| `run P`         | Find instance where P holds        |
| `run {} for N`  | Find any instance with scope N     |
| `check A`       | Find counterexample to assertion A |
| `check A for N` | Check with scope N                 |

## Where to Go Next

This guide covered Alloy syntax comprehensively. For practical application:

1. [**Alloy Basics**](/formal-methods/alloy-basics) — If you skipped it, the gentle introduction provides context
2. [**MacAlloy**](/formal-methods/macalloy) — Native macOS tool for running specifications
3. [**AD Security Model**](/formal-methods/alloy-specification) — Real-world Alloy for Active Directory security
4. [**Software Abstractions**](https://softwareabstractions.org/) — Daniel Jackson's definitive book
5. [**Alloy Documentation**](https://alloytools.org/documentation.html) — Official reference

The best way to learn is to model something you care about. Start small, run frequently, and let the Analyzer show you what your model actually allows.