Skip to main content
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.

​
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 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. 
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 closuref.^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 or 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.
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.

​
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. 
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.
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 to run this example.
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.
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.

​
Fixing the Bug

The fix depends on your requirements. Maybe you want to check destination permissions before allowing moves: 
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.
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.

​
Example 3: Network Reachability

Let’s see Alloy applied to a different domain, network topology, and introduce a few more concepts. 
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 to API permission models.

​
Core Vocabulary

Let’s solidify the concepts you’ve learned:
TermMeaning
AtomAn indivisible entity (File0, User1, etc.)
SignatureA type definition: what kinds of atoms exist
RelationA connection between atoms (fields in signatures)
FactA constraint that always holds
PredicateA reusable, parameterized formula
FunctionA parameterized expression that returns a value
AssertionA property you claim should always be true
InstanceA concrete assignment of atoms and relations
CounterexampleAn 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+. They’re complementary:
AspectAlloyTLA+
FocusStructural relationshipsState transitions over time
VerificationSAT-based bounded searchExhaustive model checking
StrengthFinding counterexamples, visualizationTemporal 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 - Comprehensive coverage of operators, quantifiers, temporal features, and everything you need for production specifications.
  2. MacAlloy - If you’re on macOS, this is the native tool I wrote for running Alloy specifications. Clean interface, fast feedback.
  3. Software Abstractions - Daniel Jackson’s book, the definitive guide to Alloy and lightweight formal methods.
  4. Alloy Documentation - 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.