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

# MacTLA

> A native macOS TLA+ verification toolbox with built-in model checking and state visualization

MacTLA is a native macOS TLA+ verification toolbox built in Swift, providing a complete specification and model checking environment without external dependencies. It implements the full TLA+ language with a BFS model checker, PlusCal translation, and interactive state graph visualization.

## Platform Overview

Unlike the Java-based TLC model checker, MacTLA is built entirely in Swift using a from-scratch implementation of the TLA+ toolchain:

| Component          | Implementation                                       |
| ------------------ | ---------------------------------------------------- |
| Lexer              | Complete TLA+ tokenizer with operator support        |
| Parser             | Recursive descent parser for full TLA+ syntax        |
| Interpreter        | Expression evaluator with environment bindings       |
| Model Checker      | BFS state exploration with temporal properties       |
| Proof Checker      | TLAPS-style theorem proving with obligation tracking |
| PlusCal Translator | Algorithm-to-TLA+ conversion                         |
| Visualizer         | Force-directed state graph with pan/zoom             |

<Info>
  MacTLA runs entirely on-device with no network dependencies, making it suitable for air-gapped environments and offline formal verification workflows.
</Info>

## Architecture

MacTLA follows an MVVM architecture, separating the TLA+ toolchain from the user interface:

<img src="https://mintcdn.com/alchemicalchef/QAt3BzspCeamWVwj/images/TLADiag.png?fit=max&auto=format&n=QAt3BzspCeamWVwj&q=85&s=76e1ad4d600d5a6f5d9270760e419221" alt="MacTLA Architecture Diagram" width="3586" height="336" data-path="images/TLADiag.png" />

### Core Components

**Lexer**: Tokenizes TLA+ source into a stream of tokens including all standard operators (`/\`, `\/`, `\A`, `\E`, `[]`, `<>`, `~>`, etc.) and keywords.

**Parser**: Recursive descent parser produces a complete abstract syntax tree (AST) representing modules, declarations, operators, and expressions.

**Interpreter**: Evaluates TLA+ expressions in given environments, supporting set operations, function application, quantifiers, and recursion with depth limiting.

**Model Checker**: Swift actor performing async BFS state space exploration with invariant checking, deadlock detection, counterexample generation, and cancellation support for long-running verifications.

**PlusCal Translator**: Converts PlusCal algorithm blocks into pure TLA+ specifications for model checking.

**Proof Checker**: TLAPS-style proof verification with theorem parsing, obligation generation, and hierarchical proof step validation.

## Model Checker Implementation

MacTLA includes a production-grade explicit-state model checker implementing TLC-style verification:

### State Exploration

**Breadth-First Search**: Systematic exploration of the state space level by level, ensuring shortest counterexamples are found first.

**Initial State Generation**: Computes all states satisfying the `Init` predicate as starting points for exploration.

**Next-State Relation**: Applies the `Next` action to generate successor states, detecting when no successors exist (deadlock).

**State Hashing**: Efficient duplicate state detection using hash-based state storage.

**Async Execution**: Verification runs asynchronously as a Swift actor, keeping the UI responsive during long-running checks. Users can cancel verification at any time without losing progress information.

**Error Reporting**: Detailed diagnostics for verification failures including the specific invariant violated, the state where violation occurred, and actionable suggestions for debugging.

### Property Checking

| Property Type    | Syntax       | Semantics                                          |
| ---------------- | ------------ | -------------------------------------------------- |
| Invariant        | `Inv`        | Must hold in every reachable state                 |
| Deadlock Freedom | (automatic)  | Every state has at least one successor             |
| Always           | `[]P`        | P holds in all states of every behavior            |
| Eventually       | `<>P`        | P holds in some state of every behavior            |
| Leads-to         | `P ~> Q`     | Whenever P holds, Q eventually holds               |
| Weak Fairness    | `WF_vars(A)` | If A is continuously enabled, it eventually occurs |
| Strong Fairness  | `SF_vars(A)` | If A is repeatedly enabled, it eventually occurs   |

### Counterexample Generation

When a property violation is detected, the model checker produces a trace:

```text theme={null}
State 0 (Initial):
  x = 0
  y = 1

State 1 (Action: Increment):
  x = 1
  y = 1

State 2 (Action: Swap):  ← Invariant violated
  x = 1
  y = 0
```

### Checker Configuration

Configuration is managed through `.cfg` files or the GUI:

```text theme={null}
Workers:        1-16 parallel workers
Max States:     1,000 to 100,000,000 states
Max Depth:      Configurable trace depth limit
Deadlock:       Enable/disable deadlock checking
Constants:      Value assignments for CONSTANTS
Invariants:     Properties to check in every state
Properties:     Temporal formulas to verify
```

## Proof Checker

MacTLA includes a TLAPS-style proof system for deductive verification of TLA+ theorems.

### Theorem Declarations

The proof checker supports standard theorem constructs:

```tla theme={null}
THEOREM TypeInvariant == Spec => []TypeOK
LEMMA SafetyLemma == Init => Safe
COROLLARY Cor1 == ASSUME NEW x \in S PROVE P(x)
PROPOSITION Prop1 == A => B
```

### Proof Syntax

Proofs can be structured hierarchically with numbered steps:

```tla theme={null}
THEOREM Consistency == Spec => []Safe
<1>1. Init => Safe
  BY DEF Init, Safe
<1>2. Safe /\ [Next]_vars => Safe'
  <2>1. CASE Action1
    BY <2>1 DEF Safe, Action1
  <2>2. CASE Action2
    BY <2>2 DEF Safe, Action2
  <2>3. QED
    BY <2>1, <2>2
<1>3. QED
  BY <1>1, <1>2, PTL DEF Spec
```

### Proof Step Types

| Step           | Purpose                                    |
| -------------- | ------------------------------------------ |
| `HAVE`         | Introduce a fact to prove                  |
| `TAKE`         | Introduce universally quantified variables |
| `WITNESS`      | Provide existential witness                |
| `PICK`         | Introduce variable satisfying condition    |
| `SUFFICES`     | Change the proof goal                      |
| `CASE`         | Proof by case analysis                     |
| `USE` / `HIDE` | Manage proof context                       |
| `DEFINE`       | Local definitions                          |
| `QED`          | Complete the proof                         |

### Proof Status

The checker tracks proof status with visual indicators:

| Status  | Meaning                        |
| ------- | ------------------------------ |
| Proved  | All obligations discharged     |
| Pending | Not yet checked                |
| Failed  | Proof obligation not satisfied |
| Trivial | Automatically verified         |
| Omitted | Explicitly marked unproven     |

### Obligation Management

Complex proofs are decomposed into proof obligations—individual goals that must be verified. The proof checker:

* Tracks hypotheses at each proof level
* Generates sub-obligations for each step
* Validates proof structure up to 100 levels deep
* Reports detailed error messages for failed proofs

## TLA+ Language Support

MacTLA implements the complete TLA+ language specification:

### Operators

**Logic**:

* `\/` (disjunction), `/\` (conjunction), `~` (negation)
* `=>` (implication), `<=>` (equivalence)

**Quantifiers**:

* `\A x \in S : P` (universal)
* `\E x \in S : P` (existential)
* `CHOOSE x \in S : P` (choice)

**Sets**:

* `\in`, `\notin`, `\subseteq`, `\cup`, `\cap`, `\`
* `SUBSET S` (powerset), `UNION S` (distributed union)
* `{x \in S : P}` (set filter), `{e : x \in S}` (set map)

**Functions**:

* `[x \in S |-> e]` (function definition)
* `f[x]` (function application)
* `DOMAIN f` (function domain)
* `[f EXCEPT ![a] = b]` (function update)

**Temporal**:

* `[]P` (always), `<>P` (eventually)
* `[]<>P` (always eventually), `<>[]P` (eventually always)
* `P ~> Q` (leads-to)
* `WF_vars(A)` (weak fairness), `SF_vars(A)` (strong fairness)
* `P'` (next-state value)

**Extended Mathematical Operators**:

* Ordering: `\prec`, `\preceq`, `\succ`, `\succeq`
* Similarity: `\sim`, `\simeq`, `\approx`, `\cong`, `\asymp`
* Lattice: `\sqcap`, `\sqcup`, `\sqsubseteq`, `\sqsupseteq`
* Circle: `\oplus`, `\ominus`, `\otimes`, `\oslash`, `\odot`
* Other: `\cdot`, `\bullet`, `\star`, `\bigcirc`, `:>`, `@@`

### Specification Declarations

MacTLA supports formal specification declarations:

```tla theme={null}
SPECIFICATION Spec
INVARIANT TypeOK, Safety
PROPERTY Liveness, Fairness
ASSUMPTION FiniteModel
```

These declarations separate specification metadata from definitions, enabling cleaner model configurations.

### PlusCal Support

MacTLA includes a built-in PlusCal translator for algorithm specifications:

```text theme={null}
--algorithm Example
variables x = 0, y = 0;

process Worker \in 1..N
begin
  Loop:
    while TRUE do
      x := x + 1;
      Checkpoint:
        y := x;
    end while;
end process;

end algorithm;
```

The translator converts PlusCal to pure TLA+ with:

* Process interleaving semantics
* Label-based atomicity
* Automatic `pc` (program counter) variable generation

## State Visualization

MacTLA provides interactive visualization of the state space:

### Force-Directed Graph

States are rendered as a navigable graph using force-directed layout:

* **Nodes** represent states with variable assignments
* **Edges** represent transitions (actions)
* **Colors** indicate state type:
  * Green: Initial states
  * Red: Error states (invariant violation)
  * Blue: Selected state

### Interaction

* **Pan**: Drag to navigate the graph
* **Zoom**: Pinch or scroll to zoom in/out
* **Select**: Click a state to inspect its variables
* **Trace**: View counterexample as highlighted path

### Trace Viewer

For counterexamples, the trace viewer shows:

* Step-by-step state progression
* Action labels between states
* Variable diff highlighting
* Navigation controls

## IDE Features

### Editor

* Syntax highlighting for TLA+ and PlusCal
* Real-time error diagnostics
* Line numbers and minimap
* Bracket matching and auto-indentation
* Search and replace with regex support
* Auto-save with file persistence

### Code Intelligence

* Context-aware code completion
* Symbol navigator for definitions
* Go-to-definition support
* Keyboard shortcuts (⌘R to run, ⌘F to find)

### File Management

* Native macOS file dialogs
* Project organization with multiple files
* Auto-save to prevent data loss

**Supported File Types**:

| Extension | Type          | Description            |
| --------- | ------------- | ---------------------- |
| `.tla`    | Specification | TLA+ module files      |
| `.cfg`    | Configuration | Model checker settings |
| `.tlaps`  | Proof         | TLAPS proof files      |

### Built-in Templates

MacTLA includes starter templates for common distributed systems patterns:

| Template          | Description                                       |
| ----------------- | ------------------------------------------------- |
| Mutex             | Mutual exclusion protocol                         |
| Producer-Consumer | Bounded buffer coordination                       |
| Two-Phase Commit  | Distributed transaction protocol                  |
| Raft              | Consensus algorithm for replicated state machines |

Templates provide a starting point for learning TLA+ and can be customized for your specific verification needs.

## Requirements

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

## Comparison with TLC and TLAPS

| Aspect              | TLC / TLAPS               | MacTLA                 |
| ------------------- | ------------------------- | ---------------------- |
| Platform            | Java (cross-platform)     | Native macOS           |
| Interface           | Command-line / IDE plugin | Integrated GUI         |
| State Visualization | Text output               | Interactive graph      |
| PlusCal             | Separate translator       | Built-in               |
| Proof Checking      | TLAPS (separate tool)     | Built-in proof checker |
| Dependencies        | JVM required              | None (self-contained)  |
| Performance         | Highly optimized          | Optimized for macOS    |

<Tip>
  MacTLA is particularly well-suited for learning TLA+ and rapid prototyping where the interactive state visualization helps build intuition about system behavior.
</Tip>

## Example: Two-Phase Commit

```tla theme={null}
--------------------------- MODULE TwoPhaseCommit ---------------------------
EXTENDS Integers, FiniteSets

CONSTANTS RM          \* Set of resource managers

VARIABLES
  rmState,            \* State of each RM: "working", "prepared", "committed", "aborted"
  tmState,            \* Transaction manager state: "init", "committed", "aborted"
  tmPrepared          \* Set of RMs that have sent "prepared"

vars == <<rmState, tmState, tmPrepared>>

Init ==
  /\ rmState = [r \in RM |-> "working"]
  /\ tmState = "init"
  /\ tmPrepared = {}

RMPrepare(r) ==
  /\ rmState[r] = "working"
  /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
  /\ UNCHANGED <<tmState, tmPrepared>>

TMRcvPrepared(r) ==
  /\ tmState = "init"
  /\ rmState[r] = "prepared"
  /\ tmPrepared' = tmPrepared \cup {r}
  /\ UNCHANGED <<rmState, tmState>>

TMCommit ==
  /\ tmState = "init"
  /\ tmPrepared = RM
  /\ tmState' = "committed"
  /\ UNCHANGED <<rmState, tmPrepared>>

TMAbort ==
  /\ tmState = "init"
  /\ tmState' = "aborted"
  /\ UNCHANGED <<rmState, tmPrepared>>

RMCommit(r) ==
  /\ tmState = "committed"
  /\ rmState' = [rmState EXCEPT ![r] = "committed"]
  /\ UNCHANGED <<tmState, tmPrepared>>

RMAbort(r) ==
  /\ tmState = "aborted"
  /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared>>

Next ==
  \/ \E r \in RM : RMPrepare(r) \/ TMRcvPrepared(r) \/ RMCommit(r) \/ RMAbort(r)
  \/ TMCommit
  \/ TMAbort

Consistency ==
  \A r1, r2 \in RM : ~ (rmState[r1] = "committed" /\ rmState[r2] = "aborted")

Spec == Init /\ [][Next]_vars
=============================================================================
```

This specification models two-phase commit with the `Consistency` invariant ensuring no resource manager commits while another aborts. MacTLA can visualize the state space and find counterexamples if the protocol is incorrectly specified.

## Related Resources

<CardGroup cols={2}>
  <Card title="AD Tier Model TLA+ Specification" icon="file-code" href="/formal-models/tla-specification">
    Use MacTLA to verify the AD Tier Model's 10 safety invariants and explore state transitions
  </Card>

  <Card title="Formal Models Overview" icon="book" href="/formal-models/overview">
    Learn how TLA+ and Alloy specifications work together to verify AD security
  </Card>
</CardGroup>

## Source Code

MacTLA is open source and available at [github.com/AlchemicalChef/MacTLA](https://github.com/AlchemicalChef/MacTLA).