MacTLA - AlchemicalChef

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

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, 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:

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

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

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;

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

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
=============================================================================

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.

AD Tier Model TLA+ Specification

Use MacTLA to verify the AD Tier Model’s 10 safety invariants and explore state transitions

Formal Models Overview

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

Source Code

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

​Platform Overview

​Architecture

​Core Components

​Model Checker Implementation

​State Exploration

​Property Checking

​Counterexample Generation

​Checker Configuration

​Proof Checker

​Theorem Declarations

​Proof Syntax

​Proof Step Types

​Proof Status

​Obligation Management

​TLA+ Language Support

​Operators

​Specification Declarations

​PlusCal Support

​State Visualization

​Force-Directed Graph

​Interaction

​Trace Viewer

​IDE Features

​Editor

​Code Intelligence

​File Management

​Built-in Templates

​Requirements

​Comparison with TLC and TLAPS

​Example: Two-Phase Commit

​Related Resources

AD Tier Model TLA+ Specification

Formal Models Overview

​Source Code

Platform Overview

Architecture

Core Components

Model Checker Implementation

State Exploration

Property Checking

Counterexample Generation

Checker Configuration

Proof Checker

Theorem Declarations

Proof Syntax

Proof Step Types

Proof Status

Obligation Management

TLA+ Language Support

Operators

Specification Declarations

PlusCal Support

State Visualization

Force-Directed Graph

Interaction

Trace Viewer

IDE Features

Editor

Code Intelligence

File Management

Built-in Templates

Requirements

Comparison with TLC and TLAPS

Example: Two-Phase Commit

Related Resources

Source Code