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.
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 |
MacTLA runs entirely on-device with no network dependencies, making it suitable for air-gapped environments and offline formal verification workflows.
Architecture
MacTLA follows an MVVM architecture, separating the TLA+ toolchain from the user interface:
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, and counterexample generation.
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.
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:
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:
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:
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:
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:
SPECIFICATION Spec
INVARIANT TypeOK, Safety
PROPERTY Liveness, Fairness
ASSUMPTION FiniteModel
PlusCal Support
MacTLA includes a built-in PlusCal translator for algorithm specifications:
--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;
- 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
- Search and replace with regex
- 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 |
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 |
MacTLA is particularly well-suited for learning TLA+ and rapid prototyping where the interactive state visualization helps build intuition about system behavior.
Example: Two-Phase Commit
--------------------------- 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
=============================================================================
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.
Source Code
MacTLA is open source and available at github.com/AlchemicalChef/MacTLA.