MacAlloy

MacAlloy is a native macOS IDE for Alloy 6.2, providing a complete formal verification environment without external dependencies. It implements Alloy 6.2 language support with a custom CDCL SAT solver, enabling lightweight formal analysis directly on macOS.

New to Alloy? Start with Alloy Basics to learn the fundamentals, then return here to run your specifications.

Platform Overview

Unlike the Java-based Alloy Analyzer, MacAlloy is built entirely in Swift using a from-scratch implementation of the Alloy toolchain:

Component	Implementation
Parser	Recursive descent parser for Alloy 6.2 syntax
Type Checker	Full semantic analysis with symbol table
Translator	Kodkod-style relational-to-boolean encoding
SAT Solver	Native CDCL solver with VSIDS heuristic
Visualizer	Force-directed graph layout for instances

MacAlloy runs entirely on-device with no network dependencies, making it suitable for air-gapped environments and offline formal verification workflows.

Architecture

MacAlloy follows a classic compiler pipeline architecture, transforming Alloy specifications through successive stages until reaching a SAT problem that can be solved for satisfying instances.

Compilation Pipeline

Lexer: Tokenizes Alloy source into a stream of tokens with full Alloy 6.2 syntax support including temporal operators. Parser: Recursive descent parser produces an abstract syntax tree (AST) representing the model structure—signatures, fields, facts, predicates, functions, and commands. Semantic Analyzer: Performs type checking, resolves references, builds the symbol table, and validates that the model is well-formed before translation. Translator: Converts the high-level relational model into a propositional formula using Kodkod-style encoding techniques. SAT Solver: Solves the generated CNF formula to find satisfying assignments (model instances) or prove unsatisfiability. Instance Extractor: Decodes SAT assignments back into Alloy instances with concrete atoms and relations.

SAT Solver Implementation

MacAlloy includes a production-grade CDCL (Conflict-Driven Clause Learning) SAT solver implementing modern solving techniques:

Core Algorithms

Two-Watched Literals: Efficient unit propagation using the two-watched-literal scheme. Each clause maintains two watched literals; only when a watched literal becomes false does the solver examine the clause. VSIDS Decision Heuristic: Variable State Independent Decaying Sum tracks variable activity based on participation in conflicts. Variables involved in recent conflicts receive activity bumps, with periodic decay to favor recently active variables. First-UIP Conflict Analysis: When a conflict occurs, the solver analyzes the implication graph to find the First Unique Implication Point—the most recent decision level variable that alone implies the conflict. This generates a learned clause that prevents the same conflict pattern. Non-Chronological Backtracking: Rather than backtracking one level at a time, the solver jumps directly to the decision level indicated by the learned clause, pruning large portions of the search space. Luby Restart Sequence: Periodic restarts using the Luby sequence prevent the solver from getting stuck in unproductive regions of the search space while preserving learned clauses.

Solver Characteristics

Propagation:     Two-watched literals with lazy update
Decisions:       VSIDS with activity decay (0.95)
Learning:        First-UIP with clause minimization
Restarts:        Luby sequence (base: 100 conflicts)
Deletion:        Activity-based clause deletion

Relational Encoding

MacAlloy uses Kodkod-style bounded model finding to translate Alloy’s relational logic into propositional SAT:

Boolean Matrix Representation

Relations are encoded as boolean matrices where each cell represents whether a tuple belongs to the relation:

For relation r: A → B with |A| = 3, |B| = 2

     b0   b1
a0 [ x00  x01 ]
a1 [ x10  x11 ]
a2 [ x20  x21 ]

Each xij is a boolean variable: true iff (ai, bj) ∈ r

Relational Operations

The translator implements the full relational algebra:

Operation	Encoding
Union (`+`)	Disjunction of corresponding matrix cells
Intersection (`&`)	Conjunction of corresponding matrix cells
Difference (`-`)	Conjunction with negation
Join (`.`)	Existential quantification over shared column
Product (`→`)	Cartesian product of matrices
Transpose (`~`)	Matrix transposition
Transitive Closure (`^`)	Iterative squaring up to scope bound
Reflexive-Transitive Closure (`*`)	Closure plus identity relation

Multiplicity Constraints

Alloy’s multiplicity keywords translate to cardinality constraints:

one r    →  exactly one tuple in r    →  EO encoding
some r   →  at least one tuple in r   →  OR of all cells
lone r   →  at most one tuple in r    →  AMO encoding
no r     →  no tuples in r            →  AND of negated cells

Temporal Logic Support

MacAlloy implements Alloy 6’s temporal extension with full LTL (Linear Temporal Logic) support:

Trace Semantics

Temporal models are verified over traces—infinite sequences of states represented as lassos (finite prefix + repeating suffix):

State₀ → State₁ → State₂ → State₃ → State₄
                              ↑__________|
                              (loop back)

Temporal Operators

Future Operators:

after / X — in the next state
always / G — in all future states
eventually / F — in some future state
until / U — holds until another property holds
releases / R — dual of until

Past Operators:

before — in the previous state
historically — in all past states
once — in some past state
since — held since another property held
triggered — dual of since

Temporal Encoding

Temporal formulas are unrolled over a bounded number of steps with loop detection:

var sig Active in Process {}

fact SomeoneAlwaysActive {
    always some Active
}

run {} for 5 Process, 10 steps

The steps bound controls trace length. The solver searches for a lasso-shaped trace satisfying all temporal constraints.

Instance Visualization

MacAlloy provides interactive visualization of satisfying instances:

Force-Directed Layout

Instances are rendered as graphs using force-directed placement:

Atoms appear as labeled nodes
Relations appear as directed edges between nodes
Signatures determine node styling and grouping

Trace Visualization

For temporal models, the trace viewer provides:

Step-by-step state navigation
Playback controls for animation
Visual diff highlighting between states
Loop point indication

IDE Features

Editor

Syntax highlighting for Alloy 6.2 with customizable themes
Real-time error underlining as you type
Severity-based error indicators:
- Red squiggles for errors
- Orange squiggles for warnings
- Blue squiggles for hints
Line numbers and code folding
Auto-indentation

Code Intelligence

MacAlloy provides advanced code navigation and refactoring capabilities:

Document Outline: Sidebar displaying all signatures, predicates, functions, and assertions for quick navigation
Go-to-Definition: Command+Click on any symbol to jump to its declaration
Hover Information: View type information and documentation by hovering over symbols
Find All References: Locate every usage of a symbol across your specification
Symbol Renaming: Rename symbols with automatic updates to all references

Diagnostics

Parse errors with source location
Type errors with expected vs actual types
Semantic warnings (unused declarations, shadowing)
Click-to-navigate from error to source

Analysis

Run commands to find satisfying instances
Check commands to search for counterexamples
Instance enumeration with “Next” button
Scope configuration per signature

File Management

Recent files quick access menu
Drag-and-drop support for .als files
Unsaved changes detection with confirmation prompts
Native macOS file dialogs

Keyboard Shortcuts

Shortcut	Action
⌘+Click	Go to definition
⌘+Shift+F	Find all references
⌘+R	Rename symbol
⌘+N	New file
⌘+O	Open file
⌘+S	Save file

Requirements

Platform	Minimum Version
macOS	14.0 (Sonoma)
Xcode (for building)	15.0

Comparison with Alloy Analyzer

Aspect	Alloy Analyzer	MacAlloy
Platform	Java (cross-platform)	Native macOS
SAT Backend	External solvers (SAT4J, MiniSat, etc.)	Built-in CDCL solver
Dependencies	JVM required	None (self-contained)
Alloy Version	6.2	6.2
Temporal Logic	Full LTL	Full LTL
Visualization	Swing-based	SwiftUI with force-directed layout
Offline Use	Requires JVM installation	Fully self-contained

MacAlloy is particularly well-suited for education and workshops where installing Java and configuring external SAT solvers presents friction. The self-contained nature simplifies deployment.

Example: Modeling a Mutex Protocol

abstract sig Process {}

one sig P1, P2, P3 extends Process {}

var sig InCS in Process {}     -- processes in critical section
var sig Requesting in Process {} -- processes requesting access

fact Init {
    no InCS              -- initially no one in critical section
    no Requesting        -- initially no one requesting
}

pred Request[p: Process] {
    p not in Requesting
    p not in InCS
    Requesting' = Requesting + p
    InCS' = InCS
}

pred Enter[p: Process] {
    p in Requesting
    no InCS
    InCS' = InCS + p
    Requesting' = Requesting - p
}

pred Exit[p: Process] {
    p in InCS
    InCS' = InCS - p
    Requesting' = Requesting
}

pred stutter {
    InCS' = InCS
    Requesting' = Requesting
}

fact Transitions {
    always (
        (some p: Process | Request[p]) or
        (some p: Process | Enter[p]) or
        (some p: Process | Exit[p]) or
        stutter
    )
}

run { eventually some InCS } for 3 Process, 8 steps

check MutualExclusionHolds {
    always lone InCS
} for 3 Process, 10 steps

This model defines a mutual exclusion protocol as a state machine with four actions: Request (ask for access), Enter (acquire the critical section), Exit (release), and stutter (no change). The run command finds example traces, while check verifies that the safety property (at most one process in the critical section) holds for all reachable states. If the property can be violated, MacAlloy displays a counterexample trace.

AD Tier Model Alloy Specification

Use MacAlloy to analyze ACL configurations and detect privilege escalation paths

Formal Models Overview

Learn how TLA+ and Alloy specifications work together to verify AD security

Source Code

MacAlloy is open source and available at github.com/AlchemicalChef/MacAlloy.

Overview

TLA+

Alloy

AD Tier Model Specifications

Binary Analysis Series

Malware Analysis

Aviation Systems Series

Tools

Platform Overview

Architecture

Compilation Pipeline

SAT Solver Implementation

Core Algorithms

Solver Characteristics

Relational Encoding

Boolean Matrix Representation

Relational Operations

Multiplicity Constraints

Temporal Logic Support

Trace Semantics

Temporal Operators

Temporal Encoding

Instance Visualization

Force-Directed Layout

Trace Visualization

IDE Features

Editor

Code Intelligence

Diagnostics

Analysis

File Management

Keyboard Shortcuts

Requirements

Comparison with Alloy Analyzer

Example: Modeling a Mutex Protocol

AD Tier Model Alloy Specification

Formal Models Overview

Source Code

​Platform Overview

​Architecture

​Compilation Pipeline

​SAT Solver Implementation

​Core Algorithms

​Solver Characteristics

​Relational Encoding

​Boolean Matrix Representation

​Relational Operations

​Multiplicity Constraints

​Temporal Logic Support

​Trace Semantics

​Temporal Operators

​Temporal Encoding

​Instance Visualization

​Force-Directed Layout

​Trace Visualization

​IDE Features

​Editor

​Code Intelligence

​Diagnostics

​Analysis

​File Management

​Keyboard Shortcuts

​Requirements

​Comparison with Alloy Analyzer

​Example: Modeling a Mutex Protocol

​Related Resources

AD Tier Model Alloy Specification

Formal Models Overview

​Source Code

Platform Overview

Architecture

Compilation Pipeline

SAT Solver Implementation

Core Algorithms

Solver Characteristics

Relational Encoding

Boolean Matrix Representation

Relational Operations

Multiplicity Constraints

Temporal Logic Support

Trace Semantics

Temporal Operators

Temporal Encoding

Instance Visualization

Force-Directed Layout

Trace Visualization

IDE Features

Editor

Code Intelligence

Diagnostics

Analysis

File Management

Keyboard Shortcuts

Requirements

Comparison with Alloy Analyzer

Example: Modeling a Mutex Protocol

Related Resources

Source Code