Specl Guide | Daniel Tisdall

Specl is a specification language and model checker for concurrent and distributed systems. You describe what your system should do, and the model checker exhaustively explores every reachable state to verify correctness — or gives you a step-by-step counterexample showing exactly how it fails.

Specl is a modern replacement for TLA+/TLC. It has clean syntax, implicit frame semantics, dict comprehensions, a bytecode-compiled Rust engine that beats TLC on every benchmark, and a full toolchain (VSCode extension, formatter, watch mode, TLA+ translator).

Installation

git clone https://github.com/danwt/specl.git
cd specl/specl
cargo install --path crates/specl-cli

This gives you the specl command. For VSCode support, install from the Marketplace or build locally:

cargo install --path crates/specl-lsp
cd editors/vscode && npm install && npm run bundle
npx vsce package && code --install-extension specl-*.vsix

Your first spec

module Counter

const MAX: 0..10
var count: 0..10

init { count = 0 }

action Inc() { require count < MAX; count = count + 1 }
action Dec() { require count > 0; count = count - 1 }

invariant Bounded { count >= 0 and count <= MAX }

specl check Counter.specl -c MAX=3

Result: OK
  States explored: 4
  Max depth: 3
  Time: 0.00s

const MAX: 0..10 — constant, set at check time with -c MAX=3
var count: 0..10 — state variable, integers 0 through 10 inclusive
init { ... } — initial state
action Inc() — state transition. require is a guard (action can only fire when true). count = count + 1 assigns the next-state value
invariant Bounded — must hold in every reachable state. Violation produces exact trace

The checker explored all 4 reachable states (count = 0, 1, 2, 3) and verified the invariant in all of them.

Language reference

Assignment vs comparison

The single most important syntax rule:

= assigns the next-state value (inside actions)
== compares values

action SetX() { x = 5 }              // assign
invariant XIs5 { x == 5 }            // compare

Implicit frame

Variables not mentioned in an action stay unchanged. No UNCHANGED clause.

// Only 'count' changes. All other variables preserved automatically.
action Inc() { require count < MAX; count = count + 1 }

Multiple variable updates

Use and to update multiple variables:

action Transfer(amount: 1..10) {
    require alice >= amount
    alice = alice - amount
    and bob = bob + amount
}

Guards

require is a precondition. If false, the action cannot fire — the checker tries other actions.

action Eat(p: 0..2) {
    require state[p] == 1
    require fork[p] == true and fork[(p + 2) % 3] == true
    state = state | { p: 2 }
    and fork = fork | { p: false, (p + 2) % 3: false }
}

Types

Type	Example	Notes
`Bool`	`true`, `false`
`Int`	`42`, `-7`	Unbounded
`Nat`	`0`, `100`	Non-negative
`0..10`		Inclusive range
`Set[T]`	`{1, 2, 3}`	Finite set
`Seq[T]`	`[a, b, c]`	Ordered list
`Dict[K, V]`	`{k: 0 for k in 0..N}`	Map
`String`	`"red"`	String literal
`Option[T]`	`Some(x)`, `None`	Optional value
`(T1, T2)`	`(1, true)`	Tuples

Type aliases: type NodeId = 0..N

Let bindings

Local definitions within expressions:

let x = len(log[i]) in
    if x == 0 then 0 else log[i][x - 1]

Works in invariants, guards, and function bodies.

Dicts

Dicts are the workhorse. Model N processes with state:

var role: Dict[Int, Int]          // process -> role
var balance: Dict[Int, Int]       // account -> balance

init {
    role = {p: 0 for p in 0..N}
    and balance = {a: 100 for a in 0..N}
}

Update with | (merge):

role = role | {i: 2}                                          // one key
balance = balance | { from: balance[from] - amount, to: balance[to] + amount }  // multiple

Parameterized actions

The checker tries all valid parameter combinations in every reachable state:

action Transfer(from: 0..N, to: 0..N, amount: 1..MAX) {
    require from != to
    require balance[from] >= amount
    balance = balance | { from: balance[from] - amount, to: balance[to] + amount }
}

With N=2, MAX=5: every combination of from, to, amount is explored in every state. This models nondeterminism — the checker handles all interleavings.

Quantifiers

all x in 0..N: balance[x] >= 0       // universal: true if P holds for ALL x
any x in 0..N: role[x] == 2          // existential: true if P holds for SOME x

Work in invariants, guards, and any expression.

Operators

Category	Operators
Logical	`and`, `or`, `not`, `implies`, `iff`
Comparison	`==`, `!=`, `<`, `<=`, `>`, `>=`
Arithmetic	`+`, `-`, `*`, `/`, `%`
Set	`in`, `not in`, `union`, `intersect`, `diff`, `subset_of`
Sequence	`++` (concat), `head(s)`, `tail(s)`, `len(s)`, `s[lo..hi]` (slice)
Dict	`keys(d)`, `values(d)`
Set	`powerset(s)`, `union_all(s)`
Choose	`choose x in S: P(x)` (pick a value satisfying P)
Conditional	`if ... then ... else ...` (always requires else — it's an expression)

Set comprehensions

{p in 0..N if state[p] == 1}                    // filter
len({v in 0..N if votedFor[v] == i})             // count
len({v in 0..N if voted[v]}) * 2 > N + 1         // quorum check

Functions

Pure, no state modification:

func LastLogTerm(l) { if len(l) == 0 then 0 else l[len(l) - 1] }
func Quorum(n) { (n / 2) + 1 }

TLA+ comparison

TLA+	Specl
`x' = x + 1`	`x = x + 1`
`x = y` (equality)	`x == y`
`UNCHANGED <<y, z>>`	(implicit)
`/\`, `\/`, `~`	`and`, `or`, `not`
`\in`, `\notin`	`in`, `not in`
`\A x \in S: P(x)`	`all x in S: P(x)`
`\E x \in S: P(x)`	`any x in S: P(x)`
`[f EXCEPT ![k] = v]`	`f \| { k: v }`
`Init == ...`	`init { ... }`
`Next == A \/ B`	(implicit — all actions OR'd)

No primed variables, no UNCHANGED. enabled(Action), changes(var), property, fairness (weak/strong), and temporal operators (always, eventually, leads_to) parse and type-check but are not yet implemented in the model checker — safety checking only for now.

Finding bugs

module Transfer

var alice: 0..50
var bob: 0..50

init { alice = 10 and bob = 10 }

// BUG: adds money without taking from alice
action BrokenDeposit() { bob = bob + 5 }

action AliceToBob() {
    require alice >= 1
    alice = alice - 1 and bob = bob + 1
}

invariant MoneyConserved { alice + bob == 20 }

Result: INVARIANT VIOLATION
  Invariant: MoneyConserved
  Trace (2 steps):
    0: init -> alice=10, bob=10
    1: BrokenDeposit -> alice=10, bob=15

The checker finds the shortest path to the violation. The trace shows exactly which action fired and what state resulted.

Example: traffic light controller

module TrafficLight

// 0=red, 1=yellow, 2=green
var northSouth: 0..2
var eastWest: 0..2

init { northSouth = 0 and eastWest = 2 }

action NSGreen() { require northSouth == 0; require eastWest == 0; northSouth = 2 }
action NSYellow() { require northSouth == 2; northSouth = 1 }
action NSRed() { require northSouth == 1; northSouth = 0 }
action EWGreen() { require eastWest == 0; require northSouth == 0; eastWest = 2 }
action EWYellow() { require eastWest == 2; eastWest = 1 }
action EWRed() { require eastWest == 1; eastWest = 0 }

invariant NoBothGreen { not (northSouth == 2 and eastWest == 2) }
invariant SafeGreen {
    (northSouth == 2) implies (eastWest == 0)
    and (eastWest == 2) implies (northSouth == 0)
}

Guards enforce mutual exclusion: NSGreen requires eastWest == 0 and vice versa. The checker verifies no sequence of light changes can put both on green.

Example: dining philosophers

module DiningPhilosophers

// 0=thinking, 1=hungry, 2=eating
var philState: Dict[0..2, 0..2]
var fork: Dict[0..2, Bool]

init {
    philState = {p: 0 for p in 0..2}
    and fork = {f: true for f in 0..2}
}

action Hungry(p: 0..2) { require philState[p] == 0; philState = philState | { p: 1 } }

action Eat(p: 0..2) {
    require philState[p] == 1
    require fork[p] == true and fork[(p + 2) % 3] == true
    philState = philState | { p: 2 }
    and fork = fork | { p: false, (p + 2) % 3: false }
}

action Done(p: 0..2) {
    require philState[p] == 2
    philState = philState | { p: 0 }
    and fork = fork | { p: true, (p + 2) % 3: true }
}

invariant NoAdjacentEating {
    all p in 0..2: not (philState[p] == 2 and philState[(p + 1) % 3] == 2)
}

Production example: Raft consensus

Leader election and log replication (simplified excerpt — for the full async model see 17-raft-vanlightly):

module Raft

const N: Int
const MaxTerm: Int
const MaxLogLen: Int

var currentTerm: Dict[Int, Int]
var role: Dict[Int, Int]       // 0=Follower, 1=Candidate, 2=Leader
var votedFor: Dict[Int, Int]
var votesGranted: Dict[Int, Dict[Int, Bool]]
var log: Dict[Int, Seq[Int]]
var commitIndex: Dict[Int, Int]

func LastLogTerm(l) { if len(l) == 0 then 0 else l[len(l) - 1] }

action Timeout(i: 0..N) {
    require role[i] != 2
    require currentTerm[i] < MaxTerm
    currentTerm = currentTerm | {i: currentTerm[i] + 1}
    and role = role | {i: 1}
    and votedFor = votedFor | {i: i}
    and votesGranted = votesGranted | {i: {t: (t == i) for t in 0..N}}
}

action BecomeLeader(i: 0..N) {
    require role[i] == 1
    require len({k in 0..N if votesGranted[i][k]}) * 2 > N + 1
    role = role | {i: 2}
}

invariant ElectionSafety {
    all i in 0..N: all j in 0..N:
        (role[i] == 2 and role[j] == 2 and currentTerm[i] == currentTerm[j])
            implies i == j
}

specl check raft.specl -c N=2 -c MaxTerm=3 -c MaxLogLen=3 --no-deadlock

With N=2, servers are 0, 1, 2 (three servers). The full spec includes RequestVote, AppendEntries, RollbackLog, AdvanceCommitIndex, and UpdateTerm, verifying ElectionSafety, LogMatching, and CommitSafety across 1.58 million states.

More examples

The repo includes verified specifications for:

Spec	Description	States	Source
Raft	Leader election + log replication (Vanlightly's async model)	—	paper
Paxos	Single-decree Paxos (Lamport)	—	paper
Two-Phase Commit	Classic distributed commit	—
EPaxos	Egalitarian Paxos (Moraru et al.)	757K	paper
Multi-Paxos	Multi-Paxos with reconfiguration	607K
Percolator	Google's distributed transactions / snapshot isolation	4.2M	paper
Parallel Commits	CockroachDB's parallel commit protocol	13.3M	RFC
PBFT	Practical Byzantine Fault Tolerance (Castro & Liskov)	—	paper
MESI	Cache coherence protocol	—
Redlock	Redis distributed lock (Antirez)	—
EWD840	Dijkstra's termination detection	—

CLI reference

specl check spec.specl -c N=3 -c MAX=10    # set constants
specl check spec.specl --no-deadlock        # skip deadlock check
specl check spec.specl --no-parallel        # single-threaded
specl check spec.specl --threads 4          # control parallelism
specl check spec.specl --max-states 100000  # limit exploration
specl check spec.specl --fast               # fingerprint-only (10x less memory, no traces)
specl check spec.specl --por                # partial order reduction
specl check spec.specl --symmetry           # symmetry reduction
specl check spec.specl --max-depth 50       # limit BFS depth
specl check spec.specl --memory-limit 4096  # max memory in MB
specl format spec.specl --write             # format in place
specl watch spec.specl -c N=3              # re-check on file change
specl translate spec.tla -o spec.specl     # TLA+ to Specl

VSCode integration

Install from the Marketplace. Features:

Diagnostics — parse and type errors as you type
Hover — type info on mouse-over
Completion — keywords, types, declarations
Format — Shift+Option+F (macOS) / Shift+Alt+F (Linux/Windows)
Go-to-definition — Cmd+Click / F12

Format on save:

{ "[specl]": { "editor.formatOnSave": true } }

Performance

Benchmarks

Specl is faster than TLC (the standard TLA+ model checker) on all benchmarks tested. With parallel BFS, Specl can hit 1M+ states/second on typical workloads.

Why Specl is faster than TLC

TLC is a Java-based model checker dating to ~2002. It's remarkably well-engineered, but it has structural limitations that Specl's architecture avoids.

State representation. TLC represents states as sorted string arrays and uses MD5 hashing (128-bit, cryptographic). Specl uses Arc<Vec<Value>> with a cached 64-bit XOR fingerprint computed incrementally via AHash. When an action modifies only 2 of 6 variables, Specl recomputes only those 2 variable hashes and XORs the delta — TLC rehashes the entire state.

Evaluation. TLC's evaluator is a Java tree-walk interpreter: every AST node is a virtual method call, every intermediate result is boxed. Specl compiles guards, invariants, and effect expressions to a bytecode VM — a flat array of opcodes executed in a tight match loop. This eliminates recursive dispatch, reduces allocations, and plays well with CPU branch prediction.

Guard indexing. When an action has parameters (e.g., Transfer(from: 0..N, to: 0..N)), TLC evaluates the full guard for every parameter combination. Specl analyzes guard conjuncts at compile time, determines which conjuncts depend on which parameters, and evaluates them incrementally as each parameter level is bound. If the first conjunct (from != to) fails, inner parameters are never enumerated. This is a form of constraint propagation.

Invariant checking. TLC checks all invariants on every new state. Specl tracks which variables each invariant reads (as a u64 bitmask) and skips invariants when none of their relevant variables changed. On specs like Raft where most actions touch 2-3 of 6 variables, this skips 50-70% of invariant evaluations.

Dict updates. TLC's EXCEPT creates a new function object per update. Specl's Value::IntMap (a flat Vec<i64>) gives O(1) indexed dict lookups, and the bytecode VM has dedicated NestedDictUpdate opcodes that update nested dicts (e.g., votesGranted[i][j]) in a single pass without allocating intermediate dicts.

Parallel exploration. TLC supports multiple workers but uses a shared queue with lock contention. Specl uses rayon with batch processing: each thread processes a batch of states, collects successors locally, then merges. The seen-set uses DashMap (sharded concurrent hashmap) or AtomicFPSet (lock-free fingerprint set for --fast mode, 8 bytes per entry).

Operation caching. Specl maintains a per-action, thread-local direct-mapped cache keyed on (parameter_hash, read_set_xor). When the same action with the same parameters hits the same read-set values, the successor fingerprint is reconstructed via XOR decomposition without re-evaluating the action. Adaptive disabling (2048-probe warmup, 2.4% minimum hit rate threshold) ensures the cache is only used when beneficial.

Memory. TLC stores full states in a hashtable. Specl's --fast mode uses AtomicFPSet: a lock-free open-addressing hash table storing only 64-bit fingerprints (8 bytes/entry vs ~200+ bytes/state). This enables exploration of 100M+ states in ~1GB of RAM, at the cost of not being able to reconstruct counterexample traces.

State space reductions

Partial order reduction (POR). The --por flag enables stubborn set computation. For each state, Specl computes which actions are independent (don't read/write overlapping variables) and explores only a sufficient subset. This can reduce the state space by orders of magnitude for loosely-coupled processes.

Symmetry reduction. The --symmetry flag enables greedy symmetry sorting. When processes are interchangeable, Specl canonicalizes states by sorting process indices, collapsing symmetric states into one representative.

Cone of influence (COI). At compile time, Specl computes which variables each action reads and writes. Actions that cannot affect any invariant variable are skipped entirely. This is automatic and zero-overhead when all actions are relevant.

Architecture

specl/crates/
├── specl-syntax/   Lexer, parser, AST, pretty-printer
├── specl-types/    Type checker
├── specl-ir/       IR, bytecode compiler, guard indexing, COI analysis
├── specl-eval/     Tree-walk evaluator + bytecode VM
├── specl-mc/       BFS explorer, parallel via rayon, state store, operation cache
├── specl-tla/      TLA+ parser and translator
├── specl-cli/      CLI
└── specl-lsp/      Language server

The compilation pipeline: source → AST (specl-syntax) → typed AST (specl-types) → IR with compiled actions (specl-ir) → bytecode for guards/invariants/effects (specl-eval) → BFS exploration (specl-mc).

Tips

Start small. Begin with 2 processes and small bounds. State spaces grow exponentially — verify correctness first, then scale up.

Use --no-deadlock for protocols. Most distributed protocols have states where no action is enabled (all messages delivered, nothing to do). This is normal, not a bug.

Read the trace. When the checker finds a violation, each step shows the action, parameters, and resulting state. This is your debugging tool.

Bounded model checking. Constants like MaxTerm=3 bound the exploration. OK with MaxTerm=3 means no bug within that bound. Increase bounds for higher confidence.

Use --fast for large state spaces. Fingerprint-only mode uses 8 bytes/state. Can't produce traces, but tells you if a violation exists.

Use --por for independent processes. Partial order reduction dramatically shrinks the state space when processes interact infrequently.

Roadmap

Parsed but not yet in model checker:

Temporal operators (always, eventually, leads_to) — compile to IR but blocked at model checking
fairness declarations (weak/strong) — parsed, not used by checker
enabled(Action), changes(var) — parsed, not evaluated

Not yet implemented:

Module composition (EXTENDS/INSTANCE)
Recursive functions
Cranelift JIT compilation (native code generation for guards/effects — estimated 3-10x additional speedup)
Swarm verification (N independent searches with randomized strategies)
Compiled verifier (SPIN-style: generate Rust, compile with rustc, dlopen)