> ## 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 Basics

> A gentle introduction to Alloy for complete beginners. Learn why constraint-based modeling matters and write your first specifications.

You think your data model is sound. Users have permissions on files, files live in folders, everything connects properly. Then a support ticket arrives: a user can access a file they shouldn't. You trace the logic. The permission check passed. The folder hierarchy is correct. But somehow, when a file moved between folders, the permission stayed attached to the old location.

Testing wouldn't have caught this. The individual operations all work. It's the *combination*, move file, check permission, observe inconsistency, that reveals the flaw. You'd need to test every sequence of operations, and there are too many.

Alloy takes a different approach. You describe *what* should be true about your system, and Alloy searches for counterexamples, specific configurations that violate your rules. If it finds one, you have a bug. If it exhaustively searches and finds none, your model is consistent within the bounds you specified.

This guide is for complete beginners.

By the end, you'll understand why Alloy matters and have written your first specifications. For comprehensive syntax details, continue to the [Alloy Syntax Guide](/formal-methods/alloy-syntax-guide).

## What is Alloy?

Alloy is a lightweight formal modeling language created by Daniel Jackson at MIT. Unlike programming languages, you don't execute Alloy specifications—you *analyze* them. The Alloy Analyzer searches for instances that satisfy your constraints or violate your assertions.

Organizations use Alloy for critical systems:

* **Microsoft Research** has published work applying Alloy to access control policies
* **AT\&T** used Alloy to model telephone switching networks
* **Aerospace applications** include verifying spacecraft software properties

These examples come from [Software Abstractions](https://softwareabstractions.org/) and academic literature. You can find a bunch more, I just wanted to show how wide the application of this can be.

The common thread in all these is that Alloy found design flaws that would have been expensive to fix in production, inconsistencies in permission models, edge cases in protocols, and missing constraints in data schemas.

## The Mental Model

Before diving into syntax, let's build intuition.

**Atoms:** An atom is an indivisible entity a user, a file, a server. It's the smallest discrete entity that can exist. Atoms have no internal structure in Alloy, they're just distinct identities. Think of them as rows in a database with only an ID column.

**Signatures:** A signature defines a *type* of atom. `sig File {}` says "there are things called Files." When Alloy analyzes your model, it generates concrete atoms: File0, File1, File2. Signatures are like tables in a database.

**Relations:** Relations connect atoms. `sig File { parent: one Folder }` says every File has exactly one parent Folder. Relations are like foreign keys. Alloy represents all data as relations even attributes are just relations to value atoms.

**Facts:** Facts are constraints that must always hold. `fact { no f: Folder | f.parent = f }` says no folder can be its own parent. Facts eliminate impossible configurations from Alloy's search.

**Instances:** An instance is a concrete assignment of atoms and relations that satisfies all facts. When you run the Analyzer, it searches for valid instances. If your model is overconstrained, no instances exist.

**Counterexamples.** When you assert something should always be true, Alloy searches for violations. A counterexample is a specific instance that breaks your assertion proof that your model has a flaw.

## Example 1: File System Basics

Let's write a complete specification. This one models something familiar, files and folders, but introduces all the core concepts.

```alloy theme={null}
module FileSystem

sig File {
    parent: one Folder
}

sig Folder {
    parent: lone Folder
}

fact NoCircularFolders {
    no f: Folder | f in f.^parent
}

run {} for 3 File, 2 Folder
```

Let me explain each part:

`module FileSystem` - Names this specification. Modules help organize larger models.

`sig File { parent: one Folder }` - Defines the File signature. Every File has exactly one parent Folder. The keyword `one` means "exactly one."

`sig Folder { parent: lone Folder }` - Defines Folders. Each Folder has at most one parent. The keyword `lone` means "zero or one" this allows root folders with no parent.

`fact NoCircularFolders` - A constraint: no folder can be an ancestor of itself. The `^` operator means transitive closure`f.^parent` is the parent, grandparent, great-grandparent, and so on. The `in` operator tests membership.

`run {} for 3 File, 2 Folder` - Tells the Analyzer: find an instance with up to 3 Files and 2 Folders (could be fewer). The empty braces `{}` mean no additional constraints beyond the facts.

Paste this into the [Alloy Analyzer](https://alloytools.org/download.html) or [MacAlloy](/formal-methods/macalloy) and click Execute. You'll see a visualization showing concrete atoms like `File0`, `File1`, `Folder0` connected by arrows representing the `parent` relation. This isn't abstract, it's a specific, valid configuration that satisfies all your constraints.

<Tip>
  You've just written your first Alloy specification. The file system is simple, but it introduced every concept you need: signatures, relations, multiplicities, facts, and the run command.
</Tip>

## Example 2: The Permission Bug

The file system works, but it's not useful yet. Let's add users and permissions, and find a bug.

```alloy theme={null}
module FilePermissions

sig File {
    parent: one Folder
}

sig Folder {
    parent: lone Folder
}

sig User {
    canAccess: set Folder
}

fact NoCircularFolders {
    no f: Folder | f in f.^parent
}

-- A user can read a file if they can access its parent folder
pred canRead[u: User, f: File] {
    f.parent in u.canAccess
}

run canRead for 3 File, 2 Folder, 2 User
```

New concepts:

`canAccess: set Folder` - Each User can access zero or more Folders. The keyword `set` means "any number."

`pred canRead[u: User, f: File]` - A *predicate* is a reusable formula with parameters. This one says user `u` can read file `f` if `u` can access `f`'s parent folder.

`run canRead` - Find an instance where the predicate is true (some user can read some file).

This works. But there's a subtle problem. What happens when we move a file?

### Finding the Bug

In a real system, files can move between folders. Let's model that and check if permissions stay correct.

To model change over time, we need Alloy's *temporal* features. This is more advanced than what we've covered so far—don't worry if it takes a second reading. The key insight is worth the complexity: we can ask Alloy to find bugs that only appear when things change.

<Note>
  This section uses Alloy 6's temporal features (`var`, `'`, `after`, `always`). If you're using Alloy 4 or 5, these features aren't available. Download [Alloy 6](https://github.com/AlloyTools/org.alloytools.alloy/releases) to run this example.
</Note>

```alloy theme={null}
module FilePermissionsBug

sig File {
    var parent: one Folder
}

sig Folder {
    parent: lone Folder
}

sig User {
    canAccess: set Folder
}

fact NoCircularFolders {
    no f: Folder | f in f.^parent
}

pred canRead[u: User, f: File] {
    f.parent in u.canAccess
}

pred moveFile[f: File, newParent: Folder] {
    f.parent' = newParent
    all other: File - f | other.parent' = other.parent
}

-- Property: if a user could read a file before, they can still read it after moving
-- (This is WRONG and Alloy will find a counterexample!)
assert MovePreservesAccess {
    all u: User, f: File, newFolder: Folder |
        (canRead[u, f] and moveFile[f, newFolder]) implies after canRead[u, f]
}

check MovePreservesAccess for 3 File, 2 Folder, 2 User
```

New concepts:

`var parent: one Folder` - The `var` keyword marks a *mutable* relation. File parents can change over time. (This uses Alloy 6's temporal features.)

`f.parent' = newParent` - The prime (`'`) means "the value in the next state." Like TLA+, Alloy can model state transitions.

`all other: File - f | other.parent' = other.parent` - This is a *frame condition*: it explicitly says all other files keep their current parents. Without this, Alloy could change any file's parent arbitrarily in the next state.

`assert MovePreservesAccess` - An *assertion* is something you claim should always be true. The `check` command searches for violations.

`after canRead[u, f]` - The temporal operator `after` means "in the next state."

Run this specification. Alloy finds a **counterexample**:

* User0 can access Folder0
* File0's parent is Folder0 (so User0 can read it)
* File0 moves to Folder1
* User0 cannot access Folder1
* User0 can no longer read File0

The assertion fails. Moving a file can revoke access unintentionally. This is exactly the bug from our opening scenario.

<Info>
  This is Alloy's killer feature: you write down what *should* be true, and Alloy shows you exactly how it can be false. The counterexample isn't abstract, it's a specific scenario you can trace through.
</Info>

### Fixing the Bug

The fix depends on your requirements. Maybe you want to check destination permissions before allowing moves:

```alloy theme={null}
pred safeMoveFile[u: User, f: File, newParent: Folder] {
    newParent in u.canAccess  -- User must have access to destination
    f.parent' = newParent
    all other: File - f | other.parent' = other.parent
}

assert SafeMovePreservesAccess {
    all u: User, f: File, newFolder: Folder |
        (canRead[u, f] and safeMoveFile[u, f, newFolder]) implies after canRead[u, f]
}

check SafeMovePreservesAccess for 3 File, 2 Folder, 2 User
```

Now the check passes. By requiring users have access to the destination folder, we ensure they can still read the file after the move.

<Note>
  When `check` finds no counterexample, it means no violation exists *within the bounds you specified* (here, up to 3 files, 2 folders, 2 users). Alloy doesn't prove properties hold for all possible sizes—just that no small counterexample exists. In practice, most bugs manifest in small instances, making bounded verification surprisingly effective.
</Note>

## Example 3: Network Reachability

Let's see Alloy applied to a different domain, network topology, and introduce a few more concepts.

```alloy theme={null}
module NetworkReachability

abstract sig Device {}

sig Computer extends Device {
    connectedTo: set Router
}

sig Router extends Device {
    linkedTo: set Router
}

sig Server extends Device {
    hostedOn: one Router
}

-- Network links are bidirectional
fact Symmetric {
    linkedTo = ~linkedTo
}

-- All routers reachable from each other (no network partitions)
fact FullyConnected {
    all r1, r2: Router | r1 in r2.*linkedTo
}

-- Transitive closure: what can a computer reach?
fun reachableRouters[c: Computer]: set Router {
    c.connectedTo.*linkedTo
}

fun reachableServers[c: Computer]: set Server {
    { s: Server | s.hostedOn in reachableRouters[c] }
}

-- Every computer can reach every server
assert UniversalReachability {
    all c: Computer, s: Server | s in reachableServers[c]
}

check UniversalReachability for 3 Computer, 3 Router, 2 Server

run {} for 3 Computer, 3 Router, 2 Server
```

New concepts:

`abstract sig Device {}` - An abstract signature has no atoms of its own; only its extensions do. Device exists only to group Computer, Router, and Server.

`sig Computer extends Device` - Computer is a subtype of Device. Inheritance works as you'd expect.

`*linkedTo` - The `*` is reflexive transitive closure: the router itself, plus everything reachable through `linkedTo`.

`fun reachableRouters[c: Computer]: set Router` - A *function* returns a value. Here it returns all routers reachable from computer `c`.

`{ s: Server | s.hostedOn in reachableRouters[c] }` - A set comprehension: all servers whose hosting router is in the reachable set.

Run the model.

The `check` should pass, with symmetric links and full router connectivity, every computer can reach every server through some path. If you *did* get a counterexample, it would mean some computer can't reach some server. Common causes: `connectedTo` is empty (computer isn't plugged in), or the model has a bug. Try removing the `Symmetric` fact and see what happens.

This pattern, model the system, assert properties, check for violations is how I use Alloy for real designs, from [Active Directory trust relationships](/formal-methods/alloy-specification) to API permission models.

## Core Vocabulary

Let's solidify the concepts you've learned:

| Term               | Meaning                                           |
| ------------------ | ------------------------------------------------- |
| **Atom**           | An indivisible entity (File0, User1, etc.)        |
| **Signature**      | A type definition: what kinds of atoms exist      |
| **Relation**       | A connection between atoms (fields in signatures) |
| **Fact**           | A constraint that always holds                    |
| **Predicate**      | A reusable, parameterized formula                 |
| **Function**       | A parameterized expression that returns a value   |
| **Assertion**      | A property you claim should always be true        |
| **Instance**       | A concrete assignment of atoms and relations      |
| **Counterexample** | An instance that violates an assertion            |

**Key notation:**

* `one` — Exactly one (required, singular)
* `lone` — Zero or one (optional, singular)
* `some` — One or more (required)
* `set` — Zero or more (optional, plural)
* `.` — Relational join (navigation)
* `^` — Transitive closure
* `*` — Reflexive transitive closure
* `~` — Transpose (inverse)
* `in` — Membership/subset test
* `'` — Next-state value (temporal)

## Alloy vs. TLA+

You might wonder when to use Alloy versus [TLA+](/formal-methods/tla-basics). They're complementary:

| Aspect           | Alloy                                  | TLA+                                   |
| ---------------- | -------------------------------------- | -------------------------------------- |
| **Focus**        | Structural relationships               | State transitions over time            |
| **Verification** | SAT-based bounded search               | Exhaustive model checking              |
| **Strength**     | Finding counterexamples, visualization | Temporal properties, liveness          |
| **Best for**     | "Can this bad state exist?"            | "Does this sequence happen correctly?" |

Use Alloy when you want to explore structural constraints: data models, permission systems, network topologies. Use TLA+ when you care about behavior over time: protocols, distributed systems, concurrent algorithms.

I often use both for the same system Alloy for the data model, TLA+ for the protocol.

## Where to Go Next

You've learned the core concepts: signatures, relations, facts, predicates, assertions, and how Alloy finds counterexamples. You've seen three examples, from simple to moderately complex.

**Next steps:**

1. [**Alloy Syntax Guide**](/formal-methods/alloy-syntax-guide) - Comprehensive coverage of operators, quantifiers, temporal features, and everything you need for production specifications.
2. [**MacAlloy**](/formal-methods/macalloy) - If you're on macOS, this is the native tool I wrote for running Alloy specifications. Clean interface, fast feedback.
3. [**Software Abstractions**](https://softwareabstractions.org/) - Daniel Jackson's book, the definitive guide to Alloy and lightweight formal methods.
4. [**Alloy Documentation**](https://alloytools.org/documentation.html) - Official tutorials and reference material.

The goal isn't to formally verify every data model. It's to find the subtle inconsistencies in your *designs*, the permission gaps, the missing constraints, the edge cases you didn't think to test. Write a small specification, run the Analyzer, and see what it finds.