Introduction

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

What is model checking?

Distributed systems fail in subtle ways. Race conditions, message reordering, partial failures, and Byzantine faults combine to produce behaviors that no amount of unit testing will catch. The state space is too large for random testing and too complex for manual reasoning.

A model checker solves this by exhaustive exploration: given a specification of your system’s state machine, it systematically visits every reachable state and verifies that your safety properties hold in all of them. If a property is violated, you get the shortest trace — the exact sequence of actions — that leads to the bug.

This is how protocols like Raft, Paxos, and TiDB’s transaction protocol are verified. Specl makes this process accessible with clean syntax and a fast Rust engine.

Why Specl?

Specl is a modern replacement for TLA+/TLC. The key improvements:

• Clean syntax. No backslash operators (/\, \/, ~), no primed variables (x'), no UNCHANGED. Just and, or, not, = for assignment, == for comparison.
• Implicit frame semantics. Variables not mentioned in an action stay unchanged automatically.
• Dict comprehensions. The workhorse for modelling N processes with per-process state.
• Fast Rust engine. Bytecode-compiled VM, parallel BFS, incremental fingerprinting. Beats TLC on every benchmark.
• Full toolchain. VSCode extension with diagnostics/completion/hover, formatter, watch mode, TLA+ translator.

Quick comparison with TLA+

If you’re new to model checking, start with Your First Spec. If you’re coming from TLA+, see the full TLA+ Comparison.

Installation

Specl is distributed as a Rust crate. You need a working Rust toolchain.

Install from source

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

This gives you the specl command.

Verify the installation

specl --version

VSCode extension

For editor support (diagnostics, hover, completion, formatting), install from the VS Marketplace.

Or build from source:

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

See Editor Setup for configuration details.

Your First Spec

Here is a complete Specl specification — a bounded counter:

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 }

Save this as counter.specl and run:

specl check counter.specl -c MAX=3

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

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

What each line means

• module Counter — every spec is a module with a name.
• const MAX: 0..10 — a constant. Its value is set at check time with -c MAX=3. The type 0..10 means integers from 0 to 10 inclusive.
• var count: 0..10 — a state variable. This is the state that the checker tracks.
• init { count = 0 } — the initial state. All variables must be assigned.
• action Inc() — a state transition. require count < MAX is a guard: the action can only fire when the condition is true. count = count + 1 assigns the next-state value.
• action Dec() — another transition. The checker tries all enabled actions in every reachable state.
• invariant Bounded — a property that must hold in every reachable state. If violated, the checker produces the shortest trace to the violation.

Key syntax rules

Two things to internalize immediately:

1. = assigns, == compares. Inside actions, x = 5 sets the next-state value. In invariants and guards, x == 5 tests equality.

2. Implicit frame. Variables not mentioned in an action stay unchanged. No UNCHANGED clause is needed. In the Inc action above, only count changes — if there were other variables, they would be preserved automatically.

Running the Checker

Basic usage

specl check spec.specl -c N=3

The -c flag sets constant values. You can pass multiple constants:

specl check spec.specl -c N=3 -c MAX=10

Understanding the output

OK — all states verified

Result: OK
  States explored: 1,580,000
  Distinct states: 1,580,000
  Max depth: 47
  Time: 19.0s (83K states/s)

All reachable states satisfy all invariants. No deadlocks were found (unless --no-deadlock was used).

Invariant violation

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

The checker found the shortest path to the violation. Each step shows which action fired and the resulting state. This trace is your primary debugging tool.

Deadlock

Result: DEADLOCK
  Trace (N steps):
    ...

A reachable state where no action is enabled. For protocols this is often expected — use --no-deadlock to suppress deadlock checking.

Common flags

specl check spec.specl --no-deadlock        # skip deadlock detection
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 --threads 4          # control parallelism
specl check spec.specl --max-states 100000  # limit exploration

See Performance Flags for a complete reference.

Watch mode

Re-run the check automatically when the file changes:

specl watch spec.specl -c N=3

Other commands

specl format spec.specl --write    # format in place
specl lint spec.specl              # fast syntax + type check (no model checking)
specl info spec.specl -c N=3       # analyze spec: actions, state space estimates

See Advanced Commands for the full CLI reference.

Editor Setup

VSCode

Install the Specl extension from the VS Marketplace.

Features

• Diagnostics — parse and type errors as you type
• Hover — type information on mouse-over
• Completion — keywords, types, and declarations
• Go-to-definition — Cmd+Click / F12
• Find all references — Shift+F12
• Rename — F2
• Format — Shift+Option+F (macOS) / Shift+Alt+F (Linux/Windows)
• Document symbols — outline view of all declarations
• Inlay hints — parameter names shown inline at call sites
• Code lens — reference counts above action and function declarations
• Signature help — parameter info when typing action/function calls
• Call hierarchy — incoming/outgoing call relationships
• Semantic highlighting — keywords, types, variables, functions

Format on save

Add to your settings.json:

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

Building from source

If you prefer to build locally:

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

Finding Bugs

The real value of a model checker is not proving things correct — it’s finding bugs you didn’t know existed. Here’s how that works in practice.

A broken transfer protocol

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 }

Run it:

specl check transfer.specl

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

The checker found the shortest path to the violation. The BrokenDeposit action creates money from nothing — exactly the kind of bug that a unit test might miss if it only tested AliceToBob.

Reading traces

Each line in the trace shows:

1. Step number — 0 is always the initial state
2. Action name — which action fired (with parameters, if any)
3. Resulting state — the values of all variables after the action

The trace is minimal: the checker uses BFS, so it always finds the shortest path to any violation. This makes traces easy to read and reason about.

Fixing the bug

The fix is straightforward — BrokenDeposit should deduct from Alice:

action Deposit() {
    require alice >= 5
    alice = alice - 5 and bob = bob + 5
}

Re-run and the checker reports OK.

The pattern

1. Write a spec with the behavior you want to model
2. Write invariants that express what “correct” means
3. Run the checker
4. If it finds a violation, read the trace and fix the spec (or realize your invariant is wrong)
5. Iterate

This feedback loop is fast — for most specs the checker runs in under a second.

Traffic Light Controller

This example models a traffic light intersection and verifies that conflicting directions never have green simultaneously.

The spec

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)
}

How the guards enforce safety

The key insight is in NSGreen and EWGreen: each requires the other direction to be red (== 0) before going green. The checker verifies this by exploring every possible sequence of light changes and confirming no interleaving violates the invariants.

Running it

specl check traffic-light.specl

The state space is small (only 9 reachable states from the 3x3 grid of light combinations), but the checker proves that no sequence of transitions can ever reach a state where both directions are green.

What this teaches

• Guards as safety mechanism. The require statements are not just preconditions — they define the allowed transitions. The checker verifies that the guard structure is sufficient to maintain the invariants.
• Multiple invariants. NoBothGreen is a simple prohibition; SafeGreen is a stronger property using implies. Both are checked in every reachable state.
• Encoding enums as integers. 0=red, 1=yellow, 2=green is a common Specl pattern. Use comments to document the mapping.

Dining Philosophers

The dining philosophers problem is a classic concurrency exercise: three philosophers sit around a table, each with a fork on either side. To eat, a philosopher needs both adjacent forks. The challenge is ensuring no two adjacent philosophers eat simultaneously.

The spec

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)
}

Key language features demonstrated

Parameterized actions

action Hungry(p: 0..2) — the checker tries this action with every value of p (0, 1, 2) in every reachable state. This models nondeterminism: any philosopher can become hungry at any time.

Dict comprehensions

{p: 0 for p in 0..2} creates a dict {0: 0, 1: 0, 2: 0}. This is the standard way to initialize per-process state.

Dict update with |

philState = philState | { p: 2 } updates only key p, leaving other entries unchanged. The | operator merges the right-hand dict into the left.

Multi-key dict update

fork = fork | { p: false, (p + 2) % 3: false } updates two keys in a single expression.

Modular arithmetic

(p + 2) % 3 maps philosopher p to their left fork. For 3 philosophers arranged in a circle, this gives the correct wraparound.

Running it

specl check dining-philosophers.specl --no-deadlock

--no-deadlock is needed because this spec can deadlock (all philosophers hungry, all forks taken). That’s a real property of the dining philosophers problem — the spec is correct in modelling it.

How to Think About Modelling

A spec defines a state machine: an initial state, a set of actions (transitions), and invariants (safety properties). The model checker exhaustively explores every reachable state via BFS. If an invariant is violated, it produces the shortest trace leading to the violation.

The modelling process

1. Identify the state

What variables fully describe the system? For N processes, use Dict[Int, ...] keyed by process ID.

var role: Dict[Int, Int]         // per-process role (e.g., 0=follower, 1=candidate, 2=leader)
var log: Dict[Int, Seq[Int]]     // per-process log
var msgs: Set[Seq[Int]]          // message set (global)

2. Identify the actions

What can happen? Each action is a possible state transition. Use parameters to model nondeterminism — which process acts, which message is received, what value is chosen.

action Timeout(i: 0..N) { ... }           // any process can time out
action SendVote(src: 0..N, dst: 0..N) { ... }  // any pair can communicate
action ChooseValue(v: 0..MAX) { ... }      // nondeterministic choice

3. Write guards

require restricts when actions can fire. This is where you encode protocol preconditions.

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

4. Write invariants

What must always hold? Safety properties go here.

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
}

5. Start small

State spaces grow exponentially. Always start with N=2 and small bounds, verify correctness, then scale up for higher confidence.

specl check spec.specl -c N=2 -c MaxTerm=1    # start here
specl check spec.specl -c N=2 -c MaxTerm=2    # scale up
specl check spec.specl -c N=3 -c MaxTerm=2 --por --fast  # go bigger

Common patterns

Process ensemble

Model N processes with per-process state via dicts:

var state: Dict[Int, Int]
init { state = {i: 0 for i in 0..N} }
action Transition(p: 0..N) { state = state | {p: newVal} }

Message passing

Encode messages as sequences (fields packed into a tuple), store in a set:

var msgs: Set[Seq[Int]]
init { msgs = {} }

// Message types: [1, src, dst, term] = RequestVote
action SendRequestVote(src: 0..N, dst: 0..N) {
    require role[src] == 1
    msgs = msgs union {[1, src, dst, currentTerm[src]]}
}

action ReceiveRequestVote(src: 0..N, dst: 0..N, term: Int) {
    require [1, src, dst, term] in msgs
    // Process request...
}

Quorum checks

// Simple majority
len({i in 0..N if voted[i]}) * 2 > N + 1

// Byzantine quorum (N = 3f+1, need 2f+1)
len({i in 0..N if certified[i]}) >= (N * 2) / 3 + 1

Encoding enums as integers

// 0=follower, 1=candidate, 2=leader
var role: Dict[Int, 0..2]
action BecomeCandidate(i: 0..N) { require role[i] == 0; role = role | {i: 1} }

Nondeterministic choice

Use action parameters — the checker explores all possible values:

action ChooseValue(v: 0..MAX) {
    require chosen == -1
    chosen = v
}

Bounding collections

Prevent state space explosion by bounding queues:

action Send(msg: Seq[Int]) {
    require len(msgs) < MAX_MSGS
    msgs = msgs union {msg}
}

State space scaling

Use specl estimate spec.specl -c N=3 to get a rough estimate before running the full check.

Module Structure

Every Specl specification is a module. A module contains declarations in this order:

module Name

const C: Int              // constants, set at check time
var x: 0..10              // state variables with type bounds

type NodeId = 0..N        // type aliases (optional)

init { x = 0 }            // initial state (exactly one)

action Step() { ... }     // state transitions (one or more)

func Helper(a) { ... }    // pure functions (optional)

invariant Safe { ... }    // safety properties (one or more)

Module name

The module declaration must be the first non-comment line. The name is for documentation only — it does not affect the checker.

module TwoPhaseCommit

Declaration order

Within a module, declarations can appear in any order. Constants, variables, types, init, actions, functions, and invariants can be interleaved. The convention above is just a stylistic recommendation.

Comments

Line comments use //. Block comments use /* ... */.

// This is a line comment

/* This is a
   block comment */

Constants and Variables

Constants

Constants are values fixed for a given check run. Set them with -c on the command line.

const N: Int
const MAX: 0..10
const TIMEOUT: Nat

specl check spec.specl -c N=3 -c MAX=5 -c TIMEOUT=10

Constants can be used in type expressions, action parameters, and any expression throughout the spec.

Variables

Variables are the state that the model checker tracks. Each variable has a name and a type.

var count: 0..10
var active: Bool
var log: Seq[Int]
var role: Dict[Int, Int]

Type bounds matter

The type of a variable determines the possible values the checker considers. Use the tightest bounds possible to keep the state space small.

// Tight — state space: 6 values per variable
var phase: 0..5

// Loose — state space: unbounded, may not terminate
var phase: Int

Initial values

Every variable must be assigned in the init block.

init {
    count = 0
    and active = true
    and log = []
    and role = {p: 0 for p in 0..N}
}

Use and to assign multiple variables. Use ; between statements in init blocks when needed.

Types

Primitive types

Range types

L..H — integers from L to H inclusive.

var count: 0..10        // values 0, 1, 2, ..., 10
var phase: 0..3         // values 0, 1, 2, 3
const N: 1..5           // N can be 1 through 5

Ranges can use constants:

const N: Int
var index: 0..N         // depends on the value of N at check time

Range expressions in parameters cannot use arithmetic. Use a constant instead:

// Invalid
action Act(i: 0..N+1) { ... }

// Valid
const LIMIT: Int
action Act(i: 0..LIMIT) { ... }

Compound types

Set[T]

Finite sets.

var voters: Set[Int]
init { voters = {} }                          // empty set
init { voters = {1, 2, 3} }                   // literal
init { voters = {x in 0..N if active[x]} }    // comprehension

Seq[T]

Ordered sequences (0-indexed).

var log: Seq[Int]
init { log = [] }                  // empty
init { log = [1, 2, 3] }          // literal

Dict[K, V]

Maps from keys to values. The primary data structure for modelling per-process state.

var role: Dict[Int, Int]
init { role = {p: 0 for p in 0..N} }    // comprehension

See the dedicated Dicts page for full details.

Option[T]

Optional values.

var leader: Option[Int]
init { leader = None }

action Elect(i: 0..N) {
    leader = Some(i)
}

(T1, T2) — Tuples

var pair: (Int, Bool)
init { pair = (0, true) }

Type aliases

Give a name to a type expression for readability:

type NodeId = 0..N
type Role = 0..2
type Log = Seq[Int]

var currentTerm: Dict[NodeId, Nat]
var role: Dict[NodeId, Role]
var log: Dict[NodeId, Log]

Assignment vs Comparison

The single most important syntax rule in Specl:

• = assigns the next-state value (inside actions and init)
• == compares values (everywhere)

action SetX() { x = 5 }              // assign x to 5
invariant XIs5 { x == 5 }            // check if x equals 5

In actions

= on the left side of a variable sets its next-state value:

action Inc() {
    count = count + 1              // next-state count = current count + 1
}

The right-hand side count reads the current state. The left-hand side count writes the next state. This is similar to TLA+’s count' = count + 1, but without the prime notation.

In guards and invariants

== tests equality. It is a boolean expression:

action Act() {
    require role[i] == 2           // guard: only fire if role[i] is 2
    ...
}

invariant Safe { x == y }          // check: x equals y in every state

Common mistake

Using = when you meant ==, or vice versa:

// WRONG: this assigns x to 5, not checks equality
invariant Bad { x = 5 }

// RIGHT: this checks equality
invariant Good { x == 5 }

The type checker will catch many of these errors, but it’s worth internalizing the distinction.

Implicit Frame

Variables not mentioned in an action stay unchanged automatically. There is no UNCHANGED clause.

var x: 0..10
var y: 0..10
var z: 0..10

// Only x changes. y and z are preserved automatically.
action IncX() { x = x + 1 }

In TLA+, you would write UNCHANGED <<y, z>>. In Specl, this is implicit.

Why this matters

Implicit frame semantics eliminate an entire class of bugs: forgetting to list a variable in UNCHANGED. In large specs with many variables, this is a common source of errors in TLA+. In Specl, it simply cannot happen.

When a variable does change

A variable changes only when it appears on the left side of = in an action:

action Transfer(amount: 1..10) {
    require alice >= amount
    alice = alice - amount           // alice changes
    and bob = bob + amount           // bob changes
    // all other variables unchanged
}

Actions and Init

Init block

The init block defines the initial state. Every variable must be assigned.

init {
    count = 0
    and active = true
    and role = {p: 0 for p in 0..N}
}

Use and between assignments in the init block. There is exactly one init block per module.

Actions

Actions are state transitions. The checker explores all enabled actions in every reachable state.

action Inc() {
    require count < MAX
    count = count + 1
}

An action consists of:

1. Guards (require statements) — preconditions that must be true for the action to fire
2. Assignments (=) — next-state values for variables

All require statements must come before any assignments.

Parameterized actions

Actions can take parameters. 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, the checker explores every combination of from (0,1,2), to (0,1,2), and amount (1,2,3,4,5) in every state. This models nondeterminism — the checker handles all interleavings.

Multiple variable updates

Use and to update multiple variables atomically:

action Reset() {
    x = 0
    and y = 0
    and z = 0
}

Each variable can only be assigned once per action:

// WRONG: double assignment
action Bad() {
    x = x + 1 and
    x = x - 1              // ERROR: variable 'x' assigned multiple times
}

Implicit action composition

All actions are implicitly OR’d. The checker’s next-state relation is: in every state, try all actions (with all parameter combinations), and follow each enabled one to its successor state. There is no explicit Next == Action1 \/ Action2 \/ ... like in TLA+.

Guards

require is a precondition. If the condition is false, the action cannot fire — the checker moves on to try other actions.

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

Ordering rule

All require statements must come before any assignments:

// WRONG: require after assignment
action Bad() {
    x = x + 1 and
    require y > 0              // PARSE ERROR
}

// RIGHT: all requires first
action Good() {
    require y > 0
    x = x + 1
}

Multiple guards

You can use multiple require statements. They are implicitly AND’d:

action Act(i: 0..N) {
    require role[i] == 1
    require currentTerm[i] < MaxTerm
    require len(votes[i]) * 2 > N + 1
    // ... assignments ...
}

This is equivalent to a single require with and:

require role[i] == 1 and currentTerm[i] < MaxTerm and len(votes[i]) * 2 > N + 1

Multiple separate require statements are preferred for readability.

Guards vs invariants

Guards and invariants are both boolean expressions, but they serve different purposes:

• Guards restrict when an action can fire. A false guard is normal — it means the action is not applicable in that state.
• Invariants must hold in every reachable state. A false invariant is a bug — the checker reports a violation with a trace.

Guard indexing

The checker optimizes parameterized actions by analyzing which guard conjuncts depend on which parameters. If an early guard fails, inner parameter combinations are skipped. This is automatic and does not affect the semantics.

Dicts

Dicts are the workhorse data structure in Specl. They model per-process state, mappings, and any key-value structure.

Creation

Create dicts with comprehensions:

var role: Dict[Int, Int]
var balance: Dict[Int, Int]

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

This creates {0: 0, 1: 0, 2: 0} for N=2.

Access

Access values by key:

role[i]                    // single key
votesGranted[i][j]         // nested dict

Update with | (merge)

The | operator merges a dict into another, updating only the specified keys:

// Update one key
role = role | {i: 2}

// Update multiple keys
balance = balance | { from: balance[from] - amount, to: balance[to] + amount }

Nested dict update

For nested dicts (e.g., Dict[Int, Dict[Int, Bool]]), update the inner dict:

votesGranted = votesGranted | {i: votesGranted[i] | {j: true}}

This updates votesGranted[i][j] to true without affecting other entries.

Dict operations

Empty dict initialization

{} is ambiguous — it could be an empty set or an empty dict. Specl defaults to set.

// WRONG: type error — {} inferred as empty set
var state: Dict[Int, Int]
init { state = {} }

// RIGHT: use empty range comprehension
init { state = {i: 0 for i in 1..0} }

The range 1..0 is empty, so this creates an empty dict with the correct type.

No has_key()

Specl does not have a has_key() function. Instead, pre-populate all keys and use sentinel values:

// WRONG: has_key is undefined
require not has_key(state, i)

// RIGHT: pre-populate, check sentinel
init { state = {i: 0 for i in 0..N} }     // 0 = not present
action AddKey(i: 0..N) {
    require state[i] == 0
    state = state | {i: 1}
}

Conditional comprehensions

Dict comprehensions can include conditions:

// Create dict with conditional values
var cache: Dict[Int, Int]
init {
    cache = {c: if c == 0 then 2 else 0 for c in 0..C}
}

Sets and Sequences

Sets

Finite, unordered collections with no duplicates.

Literals and comprehensions

{1, 2, 3}                                    // literal
{}                                            // empty set
{p in 0..N if state[p] == 1}                  // comprehension (filter)

Set operations

Counting pattern

Use comprehensions with len to count:

// Count processes in a given state
len({p in 0..N if role[p] == 2})

// Quorum check
len({v in 0..N if voted[v]}) * 2 > N + 1

Sequences

Ordered collections (0-indexed).

Literals

[]                     // empty
[1, 2, 3]             // literal

Sequence operations

Message passing with sequences

A common pattern is to encode messages as sequences with typed fields:

var msgs: Set[Seq[Int]]

// Message: [type, src, dst, payload]
action Send(src: 0..N, dst: 0..N) {
    msgs = msgs union {[1, src, dst, currentTerm[src]]}
}

action Receive(src: 0..N, dst: 0..N, term: Int) {
    require [1, src, dst, term] in msgs
    // process...
}

Log operations

Sequences are used for logs in consensus protocols:

var log: Dict[Int, Seq[Int]]

// Append entry
log = log | {i: log[i] ++ [value]}

// Last element
let lastTerm = if len(log[i]) == 0 then 0 else log[i][len(log[i]) - 1]

// Truncate (keep first k entries)
log = log | {i: log[i][0..k]}

Quantifiers

Universal quantifier: all

True if the predicate holds for every value in the range:

all x in 0..N: balance[x] >= 0                    // all balances non-negative
all i in 0..N: all j in 0..N: ...                  // nested: all pairs

Existential quantifier: any

True if the predicate holds for at least one value:

any x in 0..N: role[x] == 2                       // some process is leader

Usage

Quantifiers work in invariants, guards, and any expression:

invariant AllPositive { all x in 0..N: balance[x] >= 0 }

action NeedLeader() {
    require any i in 0..N: role[i] == 2
    ...
}

any is boolean only

any is a boolean quantifier — it returns true or false. You cannot use the bound variable outside the quantifier body:

// WRONG: v is not in scope outside the quantifier
let v = any v in 0..N: state[v] == 2 in
state[v]

// RIGHT: use any for boolean checks only
require any v in 0..N: state[v] == 2

To pick a specific value satisfying a predicate, use fix:

let v = fix v in 0..N: state[v] == 2

Precedence with implies

When nesting all quantifiers with implies, use parentheses to be explicit:

// Potentially confusing precedence
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

// Explicit parentheses (recommended)
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)

Functions and Let Bindings

Functions

Functions are pure — they cannot modify state. Use them for reusable logic.

func LastLogTerm(l) { if len(l) == 0 then 0 else l[len(l) - 1] }
func Quorum(n) { (n / 2) + 1 }
func Max(a, b) { if a > b then a else b }
func Min(a, b) { if a <= b then a else b }

Functions can be called from actions, invariants, guards, and other functions:

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

invariant LogConsistency {
    all i in 0..N: all j in 0..N:
        LastLogTerm(log[i]) == LastLogTerm(log[j])
            implies len(log[i]) == len(log[j])
}

Let bindings

Local definitions within expressions. Two forms:

Expression-level let ... in

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

Can be nested:

let a = foo(x) in
let b = bar(y) in
    a + b

In invariants

invariant Safe {
    all i in 0..N:
        let t = currentTerm[i] in
        t >= 0 and t <= MaxTerm
}

In guards

action Act(i: 0..N) {
    let lastIdx = len(log[i]) - 1
    require lastIdx >= 0
    require log[i][lastIdx] == currentTerm[i]
    ...
}

Let bindings improve readability by naming intermediate values and avoiding repeated subexpressions.

Operators

Complete operator reference

Logical operators

Comparison operators

Arithmetic operators

Set operators

Sequence operators

Built-in functions

Dict operators

Conditionals and Fix

Conditional expressions

if ... then ... else ... is an expression — it always requires an else branch and returns a value.

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

var cache: Dict[Int, Int]
init {
    cache = {c: if c == 0 then 2 else 0 for c in 0..C}
}

invariant Safe {
    all i in 0..N:
        if role[i] == 2 then
            len({j in 0..N if votesGranted[i][j]}) * 2 > N + 1
        else
            true
}

Since if/then/else is an expression (not a statement), it can appear anywhere a value is expected: in dict comprehensions, function bodies, guards, invariants, and assignments.

Fix expressions

fix x in S: P(x) picks a value from set S satisfying predicate P. The result is deterministic — the first satisfying element (in sorted order) is returned.

let leader = fix i in 0..N: role[i] == 2

Use fix when you need to bind a specific value to a variable, as opposed to any which only returns a boolean.

// any: boolean — does a leader exist?
require any i in 0..N: role[i] == 2

// fix: value — bind a specific leader
let leader = fix i in 0..N: role[i] == 2

Invariants and Properties

Invariants

An invariant is a boolean expression that must hold in every reachable state. If the checker finds a state where the invariant is false, it reports a violation with the shortest trace.

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

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
}

Checking specific invariants

Use --check-only to check only named invariants:

specl check spec.specl --check-only ElectionSafety

Writing good invariants

• Be specific. count >= 0 is weaker than count >= 0 and count <= MAX. The more precise the invariant, the more bugs it catches.
• Check structural properties. “At most one leader per term” catches more bugs than “leaders exist”.
• Avoid overly strict invariants for async systems. In asynchronous systems, intermediate states may violate strict synchronization invariants. Invariants should express fundamental safety properties, not implementation-specific timing assumptions.

// Too strict for async — may fail due to message delays
invariant Bad { counter == len({i in 0..N if state[i] == 1}) }

// Better — express the fundamental property
invariant Good { counter >= 0 and counter <= N }

Properties

property declarations parse and type-check but are not yet implemented in the model checker. They are intended for temporal properties.

property EventuallyLeader { eventually any i in 0..N: role[i] == 2 }

See Not Yet Implemented for the full list of parsed-but-unimplemented features.

Not Yet Implemented

The following features parse and type-check but are not yet supported by the model checker. Using them will not cause errors, but they will have no effect on verification.

Temporal operators

always P                  // P holds in every state of every behavior
eventually P              // P holds in some state of every behavior
P leads_to Q              // whenever P holds, Q eventually holds

These compile to the IR but are blocked at the model checking stage. The checker currently performs safety checking only (invariants).

Fairness declarations

fairness weak Action      // Action fires infinitely often if always enabled
fairness strong Action    // Action fires infinitely often if enabled infinitely often

Parsed and stored, but not used by the checker.

Enabled and changes

enabled(Action)           // true if Action is enabled in the current state
changes(var)              // true if var changes in this transition

Parsed and type-checked, but not evaluated.

Module composition

EXTENDS and INSTANCE (TLA+-style module composition) are not yet supported. Each spec is a single module.

Recursive functions

Functions cannot currently call themselves.

Planned future features

• Cranelift JIT — compile guards and effects to native code via Cranelift for an estimated 3-10x additional speedup
• Swarm verification — N independent searches with randomized action orderings
• Compiled verifier — SPIN-style: generate Rust source, compile with rustc, dlopen the result

How It Works

State machine semantics

A Specl specification defines a state machine:

1. State — the current values of all variables
2. Initial state — defined by the init block
3. Transitions — each action, with each valid parameter combination, defines a possible transition from one state to another
4. Properties — invariants must hold in every reachable state

Breadth-first search

The model checker explores the state space using BFS:

1. Start from the initial state
2. In each state, try all actions with all parameter combinations
3. For each enabled action (all require guards pass), compute the successor state
4. Check all invariants in the successor state
5. If the successor is new (not seen before), add it to the queue
6. Repeat until the queue is empty or a violation is found

BFS guarantees that any violation trace is the shortest possible path from the initial state to the bug.

Parallel exploration

By default, Specl uses all available CPU cores. The BFS frontier is processed in batches: each thread processes a batch of states, collects successors locally, then merges into the shared state set. The shared set uses DashMap (sharded concurrent hashmap) for lock-free concurrent access.

Use --threads N to control parallelism, or --no-parallel for single-threaded deterministic execution.

State storage

Each visited state is stored in a hash set to detect duplicates. Two modes:

• Default — full state storage. Enables counterexample trace reconstruction.
• --fast — fingerprint-only mode. Stores only a 64-bit hash per state (8 bytes vs ~200+ bytes). Cannot produce traces, but enables exploration of 100M+ states in ~1GB of RAM.

Deadlock detection

A deadlock is a reachable state where no action is enabled. By default, the checker reports deadlocks as errors. Use --no-deadlock to suppress this (common for protocol specs where quiescent states are expected).

Setting Constants and Reading Output

Setting constants

Use -c KEY=VALUE to set constant values at check time:

specl check spec.specl -c N=3 -c MAX=10 -c TIMEOUT=5

Constants must be set for every const declared in the spec. The checker will error if a constant is missing.

Output: OK

Result: OK
  States explored: 1,580,000
  Distinct states: 1,580,000
  Max depth: 47
  Time: 19.0s (83K states/s)

All reachable states satisfy all invariants. The state space has been fully explored within the given constant bounds.

• States explored — total states visited (including duplicates hit during BFS)
• Distinct states — unique states in the state set
• Max depth — longest path from initial state to any reachable state
• Time — wall clock time with throughput

Output: Invariant violation

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

The trace shows the shortest path from the initial state to the violation:

• Step 0 is always the initial state
• Each subsequent step shows the action name (with parameters if any) and the resulting variable values
• The trace is minimal — BFS guarantees no shorter path exists

Use --diff to show only the variables that changed in each step (helpful for specs with many variables).

Output: Deadlock

Result: DEADLOCK
  Trace (N steps):
    ...

A reachable state where no action is enabled. Use --no-deadlock if deadlocks are expected (most protocol specs have quiescent states).

Bounded model checking

Constants like MaxTerm=3 bound the exploration. OK with MaxTerm=3 means no bug exists within that bound — it does not prove unbounded correctness. Increase bounds for higher confidence:

specl check spec.specl -c N=2 -c MaxTerm=1    # quick smoke test
specl check spec.specl -c N=2 -c MaxTerm=2    # more coverage
specl check spec.specl -c N=2 -c MaxTerm=3    # thorough
specl check spec.specl -c N=3 -c MaxTerm=2    # more processes

Performance Flags

Complete flag reference

--fast — fingerprint mode

Stores only 64-bit fingerprints instead of full states. Uses ~25x less memory. Cannot produce counterexample traces.

specl check spec.specl -c N=3 --fast    # 8 bytes/state vs ~200 bytes

Use this when you need to verify large state spaces and a simple “violation exists” / “OK” answer is sufficient. If a violation is found, re-run without --fast to get the trace.

--por — partial order reduction

Computes stubborn sets: identifies which actions are independent (don’t read/write overlapping variables) and explores only a sufficient subset. Can reduce the state space by orders of magnitude for loosely-coupled processes.

specl check spec.specl -c N=3 --por

Most effective when processes interact infrequently (e.g., separate counters that occasionally synchronize).

--symmetry — symmetry reduction

When processes are interchangeable, canonicalizes states by sorting process indices. Collapses symmetric states into one representative.

specl check spec.specl -c N=3 --symmetry

Only effective when processes are truly identical (same actions, same initial state).

Combining flags

Flags compose freely:

# Maximum reduction for large state space
specl check spec.specl -c N=3 --por --symmetry --fast

# Bounded exploration with time limit
specl check spec.specl -c N=4 --max-states 10000000 --max-time 300

Recommended progression

# 1. Start small, default settings
specl check spec.specl -c N=2

# 2. Scale up processes
specl check spec.specl -c N=2 -c MaxTerm=2

# 3. Add reductions
specl check spec.specl -c N=2 -c MaxTerm=2 --por

# 4. Go bigger with fast mode
specl check spec.specl -c N=3 -c MaxTerm=2 --por --fast

# 5. Maximum coverage
specl check spec.specl -c N=3 -c MaxTerm=2 --por --symmetry --fast

Output Formats

Specl supports several output formats for integration with other tools.

Default (text)

Human-readable output. This is the default.

specl check spec.specl -c N=3

JSON

Machine-readable JSON output.

specl check spec.specl -c N=3 --output json

Useful for CI pipelines, scripts, and programmatic analysis of results.

ITF (Informal Trace Format)

Apalache-compatible trace format.

specl check spec.specl -c N=3 --output itf

This produces traces in the ITF format used by the Apalache model checker, enabling interoperability between tools.

Mermaid

Generates Mermaid sequence diagrams from violation traces.

specl check spec.specl -c N=3 --output mermaid

The output can be pasted into any Mermaid-compatible renderer (GitHub markdown, Mermaid Live Editor, etc.) to visualize the sequence of actions.

Graphviz DOT

Generates a full state graph in DOT format.

specl check spec.specl -c N=2 --output dot

Only practical for small state spaces (< 100 states). Render with:

specl check spec.specl -c N=2 --output dot | dot -Tpng -o states.png

Diff mode

Not an output format per se, but --diff modifies the default text output to show only changed variables in each trace step:

specl check spec.specl --diff

Useful for specs with many variables where full state dumps are hard to read.

Profiling

--profile adds per-action firing counts and timing to the output:

specl check spec.specl -c N=3 --profile

Advanced Commands

Beyond specl check, the CLI provides several additional commands.

specl info — spec analysis

Analyze a spec without running the full model checker:

specl info spec.specl -c N=3

Reports actions, variables, constants, state space characteristics, and which optimizations apply.

specl estimate — state space estimation

Estimate the state space size and required resources before committing to a full run:

specl estimate spec.specl -c N=3

specl simulate — random trace simulation

Generate random execution traces without exhaustive exploration:

specl simulate spec.specl -c N=3

Useful for quick smoke testing and understanding system behavior before running the full checker.

specl test — batch checking

Check all .specl files in a directory using // Use: comments embedded in each file:

specl test examples/

Each spec file contains a comment like:

// Use: specl check this.specl -c N=2 --no-deadlock

The test command reads these comments and runs each spec with the specified flags. Useful for CI and regression testing.

specl lint — fast validation

Quick syntax and type check without running the model checker:

specl lint spec.specl

Catches parse errors and type errors without exploring any states.

specl format — code formatter

Format a spec file:

specl format spec.specl --write    # format in place
specl format spec.specl            # print formatted output to stdout

specl watch — file watcher

Re-run the check automatically when the file changes:

specl watch spec.specl -c N=3

specl translate — TLA+ conversion

Convert a TLA+ specification to Specl:

specl translate spec.tla -o spec.specl

See TLA+ Comparison for details on the translation.

Showcase Overview

The showcase is a curated set of 8 examples that together cover all commonly-used language features, represent diverse domains, and range from trivial to strenuous.

Quick verification results

Strenuous checks

All showcase specs are in specl/examples/showcase/.

Peterson’s Mutual Exclusion

Peterson’s algorithm is a classic solution for mutual exclusion between two processes using only shared memory (no hardware support).

The algorithm

Each process signals intent via flag[i]=true, then yields priority by setting turn=other. A process enters the critical section only if the other’s flag is false or it’s this process’s turn.

The key insight: setting turn=other after flag=true ensures that if both processes are interested, one will see turn pointing to itself.

The spec

Source

module Peterson

// Peterson's mutual exclusion algorithm for 2 processes.
// Each process signals intent via flag[i]=true, then yields via turn=other.
// A process enters the critical section only if the other's flag is false
// or it's this process's turn.
//
// The key insight: setting turn=other AFTER flag=true ensures that
// if both processes are interested, one will see turn pointing to itself.
//
// Use: specl check peterson.specl --no-deadlock
// Verified: 17 states, 0.0s

// Process locations: 0=idle, 1=set_flag, 2=set_turn, 3=wait, 4=critical, 5=exit
var pc: Dict[0..1, 0..5]
var flag: Dict[0..1, Bool]
var turn: 0..1

init {
    pc = {p: 0 for p in 0..1};
    flag = {p: false for p in 0..1};
    turn = 0;
}

// Process wants to enter critical section: set flag
action SetFlag(p: 0..1) {
    require pc[p] == 0;
    flag = flag | {p: true};
    pc = pc | {p: 1};
}

// Yield priority to other process: set turn = 1-p
action SetTurn(p: 0..1) {
    require pc[p] == 1;
    turn = 1 - p;
    pc = pc | {p: 2};
}

// Wait until other process is not interested or it's our turn
action EnterWait(p: 0..1) {
    require pc[p] == 2;
    pc = pc | {p: 3};
}

// Check if we can enter critical section
action EnterCritical(p: 0..1) {
    require pc[p] == 3;
    require flag[1 - p] == false or turn == p;
    pc = pc | {p: 4};
}

// Stay waiting (other process has priority)
action StayWaiting(p: 0..1) {
    require pc[p] == 3;
    require flag[1 - p] == true and turn != p;
    pc = pc | {p: 3};
}

// Exit critical section: clear flag
action ExitCritical(p: 0..1) {
    require pc[p] == 4;
    flag = flag | {p: false};
    pc = pc | {p: 0};
}

// Mutual exclusion: both processes never in critical section
invariant MutualExclusion {
    not (pc[0] == 4 and pc[1] == 4)
}

What to notice

• Program counter pattern. pc: Dict[0..1, 0..5] with integer locations (0=idle through 5=exit) is a common way to model sequential protocols step by step.
• Parameterized over processes. Every action takes p: 0..1, so the checker explores both processes interleaved in all possible orderings.
• The invariant is simple. not (pc[0] == 4 and pc[1] == 4) — both processes cannot be in the critical section simultaneously.
• 17 states. Small enough to visualize the full state graph with --output dot.

specl check peterson.specl --no-deadlock

Dining Philosophers

Three philosophers sit around a circular table. Each needs both adjacent forks to eat. The spec verifies that no two adjacent philosophers can eat simultaneously.

The spec

Source

// Dining Philosophers - Parameterized version
// 3 philosophers (0, 1, 2) around a table with 3 forks.
// Each philosopher needs both adjacent forks to eat.
// Fork p is between philosopher p and philosopher (p+1)%3.
// Use: No constants needed

module DiningPhilosophers

// 0=thinking, 1=hungry, 2=eating
var philState: Dict[0..2, 0..2]
var fork: Dict[0..2, Bool]  // fork[i] = true means fork i is available

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

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

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

// Philosopher finishes eating
action Done(p: 0..2) {
    require philState[p] == 2;
    philState = philState | { p: 0 };
    fork = fork | { p: true, (p + 2) % 3: true };
}

// Safety: No two adjacent philosophers eating (they share a fork)
invariant NoAdjacentEating {
    all p in 0..2: not (philState[p] == 2 and philState[(p + 1) % 3] == 2)
}

What to notice

• Modular arithmetic. (p + 2) % 3 maps each philosopher to their left fork. With 3 philosophers in a circle, philosopher 0’s left fork is fork 2.
• Multi-key dict update. fork = fork | { p: false, (p + 2) % 3: false } updates two entries in one expression.
• Deadlock expected. This spec can deadlock (all philosophers hungry, no forks available). Use --no-deadlock.

specl check dining-philosophers.specl --no-deadlock

Two-Phase Commit

Two-Phase Commit (2PC) is the standard protocol for distributed transactions. One coordinator sends prepare, participants vote yes/no, and the coordinator decides commit (all yes) or abort (any no).

The spec

Source

module TwoPhaseCommit

// Two-Phase Commit (2PC) protocol for distributed transactions.
// One coordinator, N+1 participants. Coordinator sends prepare,
// participants vote yes/no, coordinator decides commit (all yes)
// or abort (any no). Participants apply the decision.
//
// Key invariant: all participants that decide agree on the outcome.
// If any participant commits, no participant aborts (and vice versa).
//
// Use: specl check two-phase-commit.specl -c N=2 --no-deadlock --no-auto --bfs
// Verified: N=2 -> OK (134 states, 0.0s)

const N: 0..3

// Coordinator state: 0=init, 1=waiting, 2=committed, 3=aborted
var coord_pc: 0..3

// Per-participant state: 0=init, 1=voted_yes, 2=voted_no, 3=committed, 4=aborted
var part_pc: Dict[0..N, 0..4]

// Votes received by coordinator
var vote: Dict[0..N, 0..1]  // 0=no vote yet/no, 1=yes
var voted: Dict[0..N, Bool]

init {
    coord_pc = 0;
    part_pc = {p: 0 for p in 0..N};
    vote = {p: 0 for p in 0..N};
    voted = {p: false for p in 0..N};
}

// Coordinator sends prepare (transitions to waiting)
action Prepare() {
    require coord_pc == 0;
    coord_pc = 1;
}

// Participant votes yes
action VoteYes(p: 0..N) {
    require coord_pc == 1;
    require part_pc[p] == 0;
    part_pc = part_pc | {p: 1};
    vote = vote | {p: 1};
    voted = voted | {p: true};
}

// Participant votes no
action VoteNo(p: 0..N) {
    require coord_pc == 1;
    require part_pc[p] == 0;
    part_pc = part_pc | {p: 2};
    vote = vote | {p: 0};
    voted = voted | {p: true};
}

// Coordinator decides commit (all voted yes)
action DecideCommit() {
    require coord_pc == 1;
    require all p in 0..N: voted[p] == true;
    require all p in 0..N: vote[p] == 1;
    coord_pc = 2;
}

// Coordinator decides abort (at least one voted no)
action DecideAbort() {
    require coord_pc == 1;
    require any p in 0..N: voted[p] == true and vote[p] == 0;
    coord_pc = 3;
}

// Participant applies commit decision
action ParticipantCommit(p: 0..N) {
    require coord_pc == 2;
    require part_pc[p] == 1;
    part_pc = part_pc | {p: 3};
}

// Participant applies abort decision
action ParticipantAbort(p: 0..N) {
    require coord_pc == 3;
    require part_pc[p] == 1 or part_pc[p] == 2;
    part_pc = part_pc | {p: 4};
}

// Agreement: no participant commits while another aborts
invariant Agreement {
    all i in 0..N: all j in 0..N:
        not (part_pc[i] == 3 and part_pc[j] == 4)
}

// Validity: if coordinator commits, all participants voted yes
invariant CommitImpliesAllYes {
    coord_pc == 2 implies all p in 0..N: vote[p] == 1
}

What to notice

• Quantifiers in guards. require all p in 0..N: voted[p] == true — the coordinator waits for all votes. require any p in 0..N: voted[p] == true and vote[p] == 0 — abort if any vote is no.
• implies in invariants. coord_pc == 2 implies all p in 0..N: vote[p] == 1 — if committed, all must have voted yes.
• Agreement invariant. No participant commits while another aborts — the fundamental safety property of 2PC.

specl check two-phase-commit.specl -c N=2 --no-deadlock

G-Counter CRDT

A Grow-only Counter where each process maintains a local counter. Processes increment their own counter and merge others’ state via pointwise max. The global value is the sum of all local counters.

The spec

Source

module GCounter

// G-Counter (Grow-only Counter) CRDT
// Each of N+1 processes maintains a local counter.
// Increment: process p increments its own counter.
// Merge: process p merges another process q's counter (pointwise max).
// The global counter value is the sum of all local counters.
//
// Key properties:
// - Monotonicity: the global value never decreases.
// - Convergence: if all increments stop and merges propagate, all processes agree.
//
// Use: specl check g-counter.specl -c N=2 -c Max=3 --no-deadlock
// Verified: N=2 Max=3 -> OK (188K states, 1.3s)

const N: 0..4
const Max: 1..5

// counter[p][q] = process p's view of process q's count
var counter: Dict[0..N, Dict[0..N, 0..Max]]

// Shadow variable tracking sum before each step (for monotonicity check)
var prev_sum: 0..255

func GlobalSum() {
    let s0 = counter[0][0] + counter[0][1] in
    if N >= 2 then s0 + counter[0][2]
    else s0
}

init {
    counter = {p: {q: 0 for q in 0..N} for p in 0..N};
    prev_sum = 0;
}

// Process p increments its own counter
action Increment(p: 0..N) {
    require counter[p][p] < Max;
    prev_sum = GlobalSum();
    counter = counter | {p: counter[p] | {p: counter[p][p] + 1}};
}

// Process p merges process q's state (pointwise max)
action Merge(p: 0..N, q: 0..N) {
    require p != q;
    // Only merge if q has something p doesn't know about
    require any r in 0..N: counter[q][r] > counter[p][r];
    prev_sum = GlobalSum();
    counter = counter | {p:
        {r: if counter[q][r] > counter[p][r] then counter[q][r] else counter[p][r]
         for r in 0..N}
    }
}

// Monotonicity: the global value (from any process's view) never decreases.
// We check process 0's view as representative.
invariant Monotonic {
    let cur = GlobalSum() in
    cur >= prev_sum
}

// Local monotonicity: individual counters never decrease
invariant CountersNonNegative {
    all p in 0..N: all q in 0..N: counter[p][q] >= 0
}

// Consistency: if two processes have identical views, they compute the same total
// (This is trivially true by construction, but documents the CRDT contract)
invariant SameViewSameValue {
    all p in 0..N: all q in 0..N:
        (all r in 0..N: counter[p][r] == counter[q][r])
        implies
        (let sp = counter[p][0] + counter[p][1] in
         let sq = counter[q][0] + counter[q][1] in
         if N >= 2 then sp + counter[p][2] == sq + counter[q][2]
         else sp == sq)
}

What to notice

• Nested dicts. counter: Dict[0..N, Dict[0..N, 0..Max]] — counter[p][q] is process p’s view of process q’s count.
• Nested dict update. counter = counter | {p: counter[p] | {p: counter[p][p] + 1}} — updates the inner dict for the incrementing process.
• Conditional comprehension. The Merge action uses if counter[q][r] > counter[p][r] then counter[q][r] else counter[p][r] inside a dict comprehension to compute the pointwise max.
• func and let. GlobalSum() is a pure function used in the Monotonic invariant via let cur = GlobalSum().
• Shadow variable for temporal reasoning. prev_sum tracks the previous global sum to verify monotonicity as a safety property (since temporal operators are not yet implemented).

specl check g-counter.specl -c N=2 -c Max=3 --no-deadlock

MESI Cache Coherence

The MESI protocol maintains cache coherence in multiprocessor systems. Each cache line is in one of four states: Modified, Exclusive, Shared, or Invalid. The spec verifies that no two caches hold the same value in conflicting states.

The spec

Source

module MESI

// MESI cache coherence protocol
// From: Papamarcos & Patel, "A low-overhead coherence solution for
//       multiprocessors with private cache memories" (ISCA 1984)
// C+1 cores (0..C), each with a cache line for a single address.
// Values 0..V represent possible data values.
// State encoding: 0=Invalid, 1=Shared, 2=Exclusive, 3=Modified
// Bus transactions are modeled atomically.
// Use: specl check mesi.specl -c C=2 -c V=1 --no-deadlock
// Verified: C=3 V=3 -> 144 states, all invariants OK

const C: Int
const V: Int

// Per core: cache line state (0=I, 1=S, 2=E, 3=M)
var cacheState: Dict[Int, Int]
// Per core: cached data value (-1 = not valid)
var cacheData: Dict[Int, Int]
// Memory value
var memory: Int

init {
    cacheState = {c: 0 for c in 0..C};
    cacheData = {c: -1 for c in 0..C};
    memory = 0;
}

// BusRd from Invalid when another core has M: M-holder flushes
// Both requester and M-holder go to S
action PrRdMissFromM(core: 0..C, mHolder: 0..C) {
    require core != mHolder;
    require cacheState[core] == 0;
    require cacheState[mHolder] == 3;
    cacheState = {c: (if c == core then 1
        else if c == mHolder then 1
        else cacheState[c]) for c in 0..C};
    cacheData = cacheData | {core: cacheData[mHolder]};
    memory = cacheData[mHolder];
}

// BusRd from Invalid when another core has E (no M exists): E-holder -> S
action PrRdMissFromE(core: 0..C, eHolder: 0..C) {
    require core != eHolder;
    require cacheState[core] == 0;
    require cacheState[eHolder] == 2;
    require not (any c in 0..C: c != core and cacheState[c] == 3);
    cacheState = {c: (if c == core then 1
        else if c == eHolder then 1
        else cacheState[c]) for c in 0..C};
    cacheData = cacheData | {core: memory};
}

// BusRd from Invalid when others have S only (no M or E)
action PrRdMissFromS(core: 0..C) {
    require cacheState[core] == 0;
    require any c in 0..C: c != core and cacheState[c] == 1;
    require not (any c in 0..C: c != core and (cacheState[c] == 2 or cacheState[c] == 3));
    cacheState = cacheState | {core: 1};
    cacheData = cacheData | {core: memory};
}

// BusRd from Invalid when no other cache has the line -> Exclusive
action PrRdMissNoSharers(core: 0..C) {
    require cacheState[core] == 0;
    require not (any c in 0..C: c != core and cacheState[c] != 0);
    cacheState = cacheState | {core: 2};
    cacheData = cacheData | {core: memory};
}

// Processor Write from Invalid: BusRdX
// If an M-holder exists, it flushes first
action PrWrFromInvalidWithM(core: 0..C, val: 0..V, mHolder: 0..C) {
    require core != mHolder;
    require cacheState[core] == 0;
    require cacheState[mHolder] == 3;
    memory = cacheData[mHolder];
    cacheState = {c: (if c == core then 3 else 0) for c in 0..C};
    cacheData = {c: (if c == core then val else -1) for c in 0..C};
}

// Write from Invalid, no M-holder
action PrWrFromInvalidNoM(core: 0..C, val: 0..V) {
    require cacheState[core] == 0;
    require not (any c in 0..C: c != core and cacheState[c] == 3);
    cacheState = {c: (if c == core then 3 else 0) for c in 0..C};
    cacheData = {c: (if c == core then val else -1) for c in 0..C};
}

// Processor Write from Shared: BusUpgr (invalidate other S copies)
action PrWrFromShared(core: 0..C, val: 0..V) {
    require cacheState[core] == 1;
    cacheState = {c: (if c == core then 3 else if cacheState[c] == 1 then 0 else cacheState[c]) for c in 0..C};
    cacheData = {c: (if c == core then val else if cacheState[c] == 1 then -1 else cacheData[c]) for c in 0..C};
}

// Processor Write from Exclusive: silent upgrade, no bus transaction
action PrWrFromExclusive(core: 0..C, val: 0..V) {
    require cacheState[core] == 2;
    cacheState = cacheState | {core: 3};
    cacheData = cacheData | {core: val};
}

// Processor Write from Modified: already M, just update value
action PrWrFromModified(core: 0..C, val: 0..V) {
    require cacheState[core] == 3;
    cacheData = cacheData | {core: val};
}

// Eviction from Modified: writeback to memory
action EvictModified(core: 0..C) {
    require cacheState[core] == 3;
    memory = cacheData[core];
    cacheState = cacheState | {core: 0};
    cacheData = cacheData | {core: -1};
}

// Eviction from Exclusive or Shared: silent
action EvictClean(core: 0..C) {
    require cacheState[core] == 1 or cacheState[core] == 2;
    cacheState = cacheState | {core: 0};
    cacheData = cacheData | {core: -1};
}

// SWMR: if M exists, no other valid copies
invariant SWMR {
    all c1 in 0..C: all c2 in 0..C:
        (c1 != c2 and cacheState[c1] == 3) implies cacheState[c2] == 0
}

// Exclusive exclusivity: if E exists, no other valid copies
invariant ExclusiveExclusive {
    all c1 in 0..C: all c2 in 0..C:
        (c1 != c2 and cacheState[c1] == 2) implies cacheState[c2] == 0
}

// Data coherence: all S-state caches agree with memory
invariant SharedMatchesMemory {
    all c in 0..C: cacheState[c] == 1 implies cacheData[c] == memory
}

// Data coherence: E-state cache matches memory
invariant ExclusiveMatchesMemory {
    all c in 0..C: cacheState[c] == 2 implies cacheData[c] == memory
}

What to notice

• Full dict comprehension with if/then/else. The actions use conditional comprehensions to update all caches simultaneously — when one cache takes exclusive ownership, all others invalidate.
• Hardware domain. This models a real CPU cache protocol, demonstrating that Specl works for hardware verification, not just distributed systems.
• Inherently small state space. Even with many caches, there are only 4 states per cache line, keeping the state space manageable.

specl check mesi.specl -c C=2 -c V=1 --no-deadlock

Paxos Consensus

Single-decree Paxos (Synod protocol) from Lamport’s “Paxos Made Simple”. The spec verifies that if two ballots both achieve majority acceptance, they must have proposed the same value.

The spec

Source

module Paxos

// Single-decree Paxos (Synod protocol)
// From: Lamport, "The Part-Time Parliament" / "Paxos Made Simple"
// Safety formulation based on Lamport's Voting/Paxos TLA+ specs
// N is the last acceptor index (N+1 acceptors, 0..N)
// MaxBallot is the last ballot number (0..MaxBallot)
// V is the last value index (V+1 possible values, 0..V)
// Quick BFS:       specl check paxos.specl -c N=2 -c MaxBallot=3 -c V=2 --no-deadlock --fast
//                  316K states, <1s
// Strenuous BFS:   specl check paxos.specl -c N=3 -c MaxBallot=3 -c V=2 --no-deadlock --fast
//                  3.35M states, ~9s
// Quick symbolic:  specl check paxos.specl -c N=2 -c MaxBallot=3 -c V=2 --no-deadlock --symbolic
//                  k-induction, 0.03s
// Strenuous sym:   specl check paxos.specl -c N=10 -c MaxBallot=10 -c V=3 --no-deadlock --symbolic
//                  k-induction, ~90s

const N: Int
const MaxBallot: Int
const V: Int

// Per acceptor: highest ballot promised (-1 = none)
var maxBal: Dict[Int, Int]

// Per acceptor: highest ballot voted in (-1 = never voted)
var maxVBal: Dict[Int, Int]

// Per acceptor: value of highest vote (-1 = never voted)
var maxVal: Dict[Int, Int]

// Per ballot: proposed value (-1 = not yet proposed)
var proposed: Dict[Int, Int]

// Per ballot × acceptor: has accepted?
var accepted: Dict[Int, Dict[Int, Bool]]

// A value v is safe to propose at ballot b if there exists a quorum Q
// (majority of acceptors) where all members promised b and either:
// (a) no member has ever voted, or
// (b) the highest vote among Q members below b has value v
func SafeAt(b, v) {
    any Q in powerset(0..N):
        len(Q) * 2 > N + 1
        and (all a in Q: maxBal[a] >= b)
        and (
            (all a in Q: maxVBal[a] == -1)
            or (any c in 0..MaxBallot:
                c < b
                and (all a in Q: maxVBal[a] <= c)
                and (any a in Q: maxVBal[a] == c and maxVal[a] == v)))
}

init {
    maxBal = {a: -1 for a in 0..N};
    maxVBal = {a: -1 for a in 0..N};
    maxVal = {a: -1 for a in 0..N};
    proposed = {b: -1 for b in 0..MaxBallot};
    accepted = {b: {a: false for a in 0..N} for b in 0..MaxBallot};
}

// Acceptor a promises not to participate in any ballot lower than b
action Promise(b: 0..MaxBallot, a: 0..N) {
    require b > maxBal[a];
    maxBal = maxBal | {a: b};
}

// Proposer proposes value v for ballot b (must be safe)
action Propose(b: 0..MaxBallot, v: 0..V) {
    require proposed[b] == -1;
    require SafeAt(b, v);
    proposed = proposed | {b: v};
}

// Acceptor a votes for the proposed value in ballot b
action Accept(b: 0..MaxBallot, a: 0..N) {
    require proposed[b] != -1;
    require maxBal[a] <= b;
    maxBal = maxBal | {a: b};
    maxVBal = maxVBal | {a: b};
    maxVal = maxVal | {a: proposed[b]};
    accepted = accepted | {b: (accepted[b] | {a: true})};
}

// Agreement: if two ballots both achieve majority acceptance,
// they must have proposed the same value
invariant Agreement {
    all b1 in 0..MaxBallot: all b2 in 0..MaxBallot:
        (len({a in 0..N if accepted[b1][a]}) * 2 > N + 1
         and len({a in 0..N if accepted[b2][a]}) * 2 > N + 1)
        implies proposed[b1] == proposed[b2]
}

// Validity: any proposed value is in the valid range
invariant Validity {
    all b in 0..MaxBallot: proposed[b] != -1 implies (proposed[b] >= 0 and proposed[b] <= V)
}

What to notice

• powerset and nested quantifiers. The SafeAt function iterates over all subsets of acceptors (powerset(0..N)) to find a quorum that satisfies the safety condition. This is the most complex expression in any showcase spec.
• Set comprehensions for quorum check. len({a in 0..N if accepted[b][a]}) * 2 > N + 1 counts accepted votes.
• Both BFS and symbolic. This is the best example for exercising both verification modes: BFS at N=3 (3.35M states, ~9s), symbolic at N=10 (k-induction, ~90s).

specl check paxos.specl -c N=2 -c MaxBallot=3 -c V=2 --no-deadlock

Redlock

Redlock is Redis’s distributed locking algorithm. This spec intentionally finds Martin Kleppmann’s counterexample: when a client pauses (GC, network delay) while holding locks, the locks expire, another client acquires them, and both clients believe they hold the lock.

The spec

Source

module Redlock

// Redlock distributed locking — modeled to find Kleppmann's counterexample
// From: Antirez, "Distributed locks with Redis" (2016)
// Analysis: Kleppmann, "How to do distributed locking" (2016)
// N is the last Redis instance index (N+1 instances, 0..N)
// M is the last client index (M+1 clients, 0..M)
// TTL is the lock time-to-live in ticks
// MaxTime bounds the global clock to keep state space finite
// Use: specl check redlock.specl -c N=2 -c M=1 -c TTL=3 -c MaxTime=8
// Verified: N=2 M=1 TTL=3 MaxTime=8 -> MutualExclusion VIOLATED in 15 steps
// The counterexample demonstrates Kleppmann's attack: client 0 acquires majority,
// time advances (locks expire), client 1 acquires majority, both enter Holding

const N: Int
const M: Int
const TTL: Int
const MaxTime: Int

// Global time (discrete ticks, models real/wall-clock time)
var globalTime: Int

// Per client: local clock (may lag behind global time due to pauses)
var localClock: Dict[Int, Int]

// Per client: state 0=Idle, 1=Acquiring, 2=Holding, 3=Released
var clientState: Dict[Int, Int]

// Per client: which instances the client has locked
var clientLocks: Dict[Int, Set[Int]]

// Per client: local clock value at time of acquisition start
var acquireTime: Dict[Int, Int]

// Per client: next instance index to try locking (sequential acquisition)
var nextInstance: Dict[Int, Int]

// Per instance: locked by which client (-1 = unlocked)
var instanceLock: Dict[Int, Int]

// Per instance: global time at which lock expires
var instanceExpiry: Dict[Int, Int]

func Majority() { (N + 1) / 2 + 1 }

init {
    globalTime = 0;
    localClock = {c: 0 for c in 0..M};
    clientState = {c: 0 for c in 0..M};
    clientLocks = {c: {} for c in 0..M};
    acquireTime = {c: 0 for c in 0..M};
    nextInstance = {c: 0 for c in 0..M};
    instanceLock = {i: -1 for i in 0..N};
    instanceExpiry = {i: 0 for i in 0..N};
}

// --- Time modeling ---

// Global time advances by one tick
action Tick() {
    require globalTime < MaxTime;
    globalTime = globalTime + 1;
}

// Client c's local clock advances (catches up toward global time)
// A client that never fires ClockAdvance is effectively paused
action ClockAdvance(c: 0..M) {
    require localClock[c] < globalTime;
    localClock = localClock | {c: localClock[c] + 1};
}

// --- Lock expiry ---

// Instance i's lock expires (TTL exceeded in real/global time)
action ExpireLock(i: 0..N) {
    require instanceLock[i] != -1;
    require globalTime >= instanceExpiry[i];
    instanceLock = instanceLock | {i: -1};
}

// --- Client lock acquisition ---

// Client c starts acquiring the lock
action StartAcquire(c: 0..M) {
    require clientState[c] == 0;
    clientState = clientState | {c: 1};
    acquireTime = acquireTime | {c: localClock[c]};
    clientLocks = clientLocks | {c: {}};
    nextInstance = nextInstance | {c: 0};
}

// Client c successfully locks instance i (SET NX equivalent)
action TryLock(c: 0..M, i: 0..N) {
    require clientState[c] == 1;
    require nextInstance[c] == i;
    require instanceLock[i] == -1;
    instanceLock = instanceLock | {i: c};
    instanceExpiry = instanceExpiry | {i: globalTime + TTL};
    clientLocks = clientLocks | {c: clientLocks[c] union {i}};
    nextInstance = nextInstance | {c: i + 1};
}

// Client c fails to lock instance i (already locked by another client)
action FailLock(c: 0..M, i: 0..N) {
    require clientState[c] == 1;
    require nextInstance[c] == i;
    require instanceLock[i] != -1;
    require instanceLock[i] != c;
    nextInstance = nextInstance | {c: i + 1};
}

// Client c finishes acquisition: majority obtained and validity remaining
// Validity check uses LOCAL clock (this is the source of the bug)
action FinishAcquire(c: 0..M) {
    require clientState[c] == 1;
    require nextInstance[c] > N;
    require len(clientLocks[c]) >= Majority();
    require localClock[c] - acquireTime[c] < TTL;
    clientState = clientState | {c: 2};
}

// Client c fails acquisition: unlock all instances, return to Idle
action FailAcquire(c: 0..M) {
    require clientState[c] == 1;
    require nextInstance[c] > N;
    require len(clientLocks[c]) < Majority()
        or localClock[c] - acquireTime[c] >= TTL
    clientState = clientState | {c: 0};
    clientLocks = clientLocks | {c: {}};
    instanceLock = {i:
        if instanceLock[i] == c then -1 else instanceLock[i]
        for i in 0..N}
}

// Client c releases the lock (DEL on all instances if value matches)
action ReleaseLock(c: 0..M) {
    require clientState[c] == 2;
    clientState = clientState | {c: 3};
    instanceLock = {i:
        if instanceLock[i] == c then -1 else instanceLock[i]
        for i in 0..N}
}

// --- Safety property ---

// Mutual exclusion: at most one client in Holding state
// This SHOULD be VIOLATED — the checker finds Kleppmann's counterexample
invariant MutualExclusion {
    all c1 in 0..M: all c2 in 0..M:
        (clientState[c1] == 2 and clientState[c2] == 2)
        implies c1 == c2
}

What to notice

• Intentional violation. Unlike other showcase specs, this one is designed to fail. The MutualExclusion invariant is violated — that’s the point.
• Time modelling. Global time advances via Tick(), client local clocks advance via ClockAdvance(). A client that never fires ClockAdvance is effectively paused — modelling GC pauses or network delays.
• The bug. Client checks lock validity using localClock (line 118), but locks expire based on globalTime. If a client pauses (local clock falls behind global time), its locks expire while it still thinks they’re valid.
• Set operations. clientLocks[c] union {i} for accumulating acquired locks, conditional dict comprehension for releasing all locks on failure.

specl check redlock.specl -c N=2 -c M=1 -c TTL=3 -c MaxTime=8

The checker finds the violation in 15 steps.

Raft Consensus

Raft leader election and log replication, modelled after Vanlightly’s async formulation. This is the most complex showcase spec at 386 lines, verifying ElectionSafety, LogMatching, and CommitSafety.

The spec

Source (386 lines — view on GitHub for the full spec)

Key features demonstrated

• Seq and Set[Seq[Int]] — logs are sequences, messages are sets of sequences
• Message passing — msgs is a Set[Seq[Int]] where each sequence encodes a message with fields [type, src, dst, term, ...]
• Sequence operations — ++ for log append, len(), slicing with [0..k], head(), tail()
• union / diff — adding and consuming messages
• Complex invariants — ElectionSafety (at most one leader per term), LogMatching (prefix consistency), CommitSafety (committed entries are never lost)

Running it

# Quick check (~1s)
specl check raft.specl -c N=1 -c MaxVal=0 -c MaxElections=2 \
    -c MaxRestarts=0 -c MaxLogLen=2 --no-deadlock

# Strenuous (~4 min, 166M states)
specl check raft.specl -c N=2 -c MaxVal=1 -c MaxElections=2 \
    -c MaxRestarts=0 -c MaxLogLen=3 --no-deadlock --fast

What to notice

This spec exercises nearly every Specl language feature in a single real-world protocol. If you can read and understand this spec, you can write Specl fluently.

Full Catalogue

The repository contains 100+ verified specifications in specl/examples/. The showcase contains 8 curated examples. Below is the full catalogue organized by domain.

Consensus

Distributed Transactions

Mutual Exclusion & Locking

CRDTs

Broadcast & Communication

Cache Coherence

Clock Synchronization

Replication & Consistency

Failure Detection & Recovery

Concurrent Data Structures

Classic Concurrency

Infrastructure Patterns

Hashing & Routing

Semaphore Puzzles

TLA+ Comparison

Specl is a modern replacement for TLA+/TLC. If you’re coming from TLA+, this page maps the concepts.

Syntax mapping

Key differences

No primed variables

TLA+ uses x' for the next-state value. Specl uses =:

TLA+:   Next == x' = x + 1 /\ y' = y
Specl:  action Step() { x = x + 1 }    // y unchanged implicitly

No UNCHANGED

In TLA+, every action must explicitly list unchanged variables:

TLA+:   Inc == x' = x + 1 /\ UNCHANGED <<y, z, w>>
Specl:  action Inc() { x = x + 1 }

Forgetting a variable in UNCHANGED is a common TLA+ bug. Specl eliminates this class of errors entirely.

No explicit Next

TLA+ requires an explicit Next formula that disjoins all actions:

TLA+:   Next == Inc \/ Dec \/ Reset
Specl:  // Not needed — all actions are implicitly OR'd

= vs ==

TLA+ uses = for both assignment and equality (context determines meaning). Specl separates them: = assigns, == compares.

Word-based operators

TLA+ uses symbolic operators (/\, \/, ~, \in). Specl uses words (and, or, not, in).

Translating TLA+ to Specl

Use the built-in translator:

specl translate spec.tla -o spec.specl

The translator handles most TLA+ syntax. Manual adjustments may be needed for:

• Module composition (EXTENDS, INSTANCE) — not yet supported
• Recursive operators — not yet supported
• TLA+ idioms that don’t map directly (e.g., function sets [S -> T])

Architecture and Performance

Crate structure

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-symbolic/  Symbolic verification (Z3-based)
├── specl-tla/       TLA+ parser and translator
├── specl-cli/       CLI (the `specl` binary)
└── specl-lsp/       Language server (the `specl-lsp` binary)

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)

For symbolic checking, the pipeline diverges after IR:

       → IR with compiled actions (specl-ir)
       → Z3 SMT encoding (specl-symbolic)
       → BMC / k-induction / IC3 verification

Explicit-state engine

NaN-boxed values

Runtime values are 8 bytes each, using NaN-boxing. Integers and booleans are stored inline in the NaN payload of an IEEE 754 double — no heap allocation, no pointer chasing. Collections (dicts, sets, sequences) use the remaining NaN bit patterns for a tagged Arc pointer. This eliminates the overhead of a tagged enum with a separate heap pointer for every value.

Bytecode VM and superinstructions

Specl compiles guards, invariants, and effect expressions to a bytecode VM — a flat array of opcodes executed in a tight match loop. This eliminates the recursive dispatch and boxing overhead of a tree-walk interpreter.

On top of the base bytecode, a peephole optimizer fuses common multi-opcode patterns into superinstructions. For example, VarParamDictGetIntEq fuses “load variable, load parameter, dict lookup, load integer, compare equal” into a single opcode. The optimizer profiles execution during a 2048-probe warmup phase and re-optimizes hot paths with adaptive specialization.

Current superinstructions (~15 total) cover:

• Dict lookups with parameter keys (ParamIntDictGet, VarParamDictGet2)
• Guard patterns (BoolEq, VarParamDictGetIntEq)
• Collection operations (DictUpdateN, VarParamDictGetLen)
• Sequence operations (SeqConcat, SeqSlice, SeqHead, SeqTail)
• Literal construction (SetLit, SeqLit)
• Set operations (SetUnion, SetDiff)
• Quantifier operations (Forall, Exists, SetComp over set and range domains)

State representation and hashing

States are stored as Arc<Vec<Value>> with a cached 64-bit fingerprint. Each variable’s hash is computed independently via AHash and the state fingerprint is computed by XOR-combining the variable hashes. When an action modifies only 2 of 17 variables, Specl recomputes only those 2 variable hashes and XORs the delta — an incremental update rather than a full rehash.

For comparison, TLC represents states as sorted string arrays with MD5 hashing (128-bit, cryptographic) and rehashes the entire state on every modification.

State storage

Three storage backends, automatically selected based on spec characteristics:

Full state storage (default). Uses DashMap (sharded concurrent hashmap) mapping fingerprints to full states. Supports trace reconstruction for counterexample reporting.

Fingerprint-only storage (--fast). Uses AtomicFPSet: a lock-free open-addressing hash table storing only 64-bit fingerprints (8 bytes per entry). No trace reconstruction, but enables 100M+ states in ~1GB of RAM. Uses triangular probing (probe distance grows quadratically, better clustering than linear probing) and CPU prefetch hints for cache-friendly access. Dynamic resizing prevents stalls when the load factor exceeds the threshold.

Bloom filter storage (--bloom). Uses a bloom filter for fixed-memory probabilistic state deduplication. Trades a small probability of missing states for constant memory usage regardless of state space size. Useful for specs where the state space exceeds available RAM.

Tree compression

State storage optionally uses LTSmin-style tree compression. Each variable value is stored in a shared tree node, and states that differ in only a few variables share most of their storage nodes. This reduces memory consumption and improves cache locality.

Collapse compression is also available: states are compressed into a compact byte representation by collapsing common variable-value patterns.

Guard indexing

When an action has parameters (e.g., Transfer(from: 0..N, to: 0..N)), Specl analyzes guard conjuncts at compile time. It determines which conjuncts depend on which parameters and evaluates them incrementally as each parameter level is bound. If from != to fails for a given from value, the inner to parameter is never enumerated.

State-dependent parameter domains go further: when a parameter iterates over a set stored in state (e.g., action Handle(msg: messages)), the domain is read from the current state at evaluation time, avoiding enumeration of values that aren’t present.

Invariant skipping

Specl tracks which variables each invariant reads (as a u64 bitmask). When a successor state is generated, invariants are only checked if at least one of their relevant variables changed. On specs like Raft where most actions touch 2-3 of 17 variables, this skips 50-70% of invariant evaluations.

Dict representation

Specl’s Value::IntMap is a flat Vec<i64> giving O(1) indexed dict lookups. IntMap2 is a flattened 2-level dict: a single contiguous array for Dict[0..N, Dict[0..M, T]], avoiding nested allocation. The bytecode VM has dedicated NestedDictUpdate and DictUpdateN opcodes that update nested dicts in a single pass without allocating intermediate dicts.

Parallel BFS

Specl uses rayon with batch processing: each thread processes a batch of states, collects successors into a thread-local buffer, then merges into the shared frontier. The seen-set uses either DashMap or AtomicFPSet depending on storage mode. An atomic counter tracks the seen-set size (avoiding the expensive DashMap::len() call).

Early fingerprint deduplication filters duplicate successors before constructing full State objects — avoiding allocation for states already in the seen-set.

Operation caching

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.

Action ordering

Actions are sorted by guard cost (estimated from guard complexity) so that cheap-to-reject guards are evaluated first. Guards with redundant Contains checks for state-dependent domains are stripped at compile time. A precomputed has_state_dep flag avoids runtime checks for parameter domain types.

Allocator and build optimizations

• mimalloc as the global allocator — better multi-threaded allocation performance than the system allocator.
• Profile-guided optimization (PGO) with diverse training workloads (small, medium, and large specs across different protocol types). PGO improves branch prediction accuracy in the VM dispatch loop.
• LTO (link-time optimization) and #[inline(always)] annotations on hot-path functions (expect_int, expect_bool, expect_set, value constructors).

Benchmark: effect of optimizations

On a Raft benchmark (2M states, --fast --bfs, 16 threads):

Symbolic engine

The symbolic backend (specl-symbolic) encodes Specl specs as SMT formulas and uses Z3 to verify invariants without enumerating states.

Encoding

Each Specl variable becomes a Z3 constant (or function for parameterized types). Dict types are encoded as Z3 arrays. Sets as Z3 sets. Sequences as Z3 arrays with a length variable. The init block becomes a constraint on the initial state. Each action becomes a transition relation formula: a conjunction of the guard (as a precondition) and the effects (as equalities between current-state and next-state variables). The overall transition relation is a disjunction of all action formulas.

Verification techniques

Bounded model checking (BMC). Unroll the transition relation for k steps, creating variables for each time step. Check whether the invariant can be violated at any step. If a violation is found, reconstruct a concrete counterexample trace. Depth is configurable via --bmc-depth.

k-induction. A two-phase proof:

1. Base case: check that the invariant holds for all states reachable in k steps (equivalent to BMC at depth k).
2. Inductive step: assume the invariant holds for k consecutive states, and check that it holds for the (k+1)th state.

If both phases pass, the invariant holds for all reachable states regardless of depth. Many practical invariants are 2-inductive (k=2 suffices).

CTI learning. When the inductive step fails, the counterexample-to-induction (CTI) is analyzed. If the CTI state is unreachable (determined by a BMC check), a blocking clause is added to exclude it, and induction is retried. This loop iteratively strengthens the inductive hypothesis.

IC3/PDR via CHC solving. Uses Z3’s Spacer engine to solve the verification problem as a set of constrained Horn clauses (CHC). Spacer computes inductive invariants automatically using property-directed reachability (PDR). Multiple Spacer parameter profiles (default, aggressive, flexible) are available.

Golem CHC solver. An alternative CHC backend to Z3 Spacer, available when the Golem binary is installed. Can sometimes solve problems that Spacer cannot.

Portfolio mode. Runs BMC, k-induction, and IC3 in parallel (separate threads) and takes the first result. Useful when it’s unclear which technique will work best for a given spec.

Smart cascade. The default symbolic mode. Tries techniques in order of cost: single-step induction → k-induction with CTI → IC3 → BMC. Stops as soon as one succeeds. For most small-to-medium specs, induction or k-induction succeeds in milliseconds.

Configurable solver timeout

Symbolic solver calls have a configurable timeout (--solver-timeout). This prevents individual Z3 calls from blocking indefinitely on hard instances.

State space reductions

Partial order reduction (POR)

--por computes stubborn sets using guard-based precomputation. For each state, Specl identifies which actions are independent (don’t read/write overlapping variables) and explores only a sufficient subset. The implementation uses instance-level POR with key tracking — independence is checked at the level of specific dict keys, not whole variables.

Sleep sets provide additional reduction on top of stubborn sets. When two actions are independent and one has already been explored, the other is added to the sleep set and skipped in successor states.

Symmetry reduction

--symmetry canonicalizes states by computing orbit representatives — sorting process indices when processes are interchangeable. The implementation detects symmetry groups automatically from the spec structure.

Cone of influence (COI)

At compile time, Specl computes which variables each action reads and writes. Actions that cannot affect any checked invariant variable (transitively) are skipped entirely. When --check-only is used to check a specific invariant, the COI analysis filters both actions and invariant checks. Automatic and zero-overhead.

Alternative exploration modes

Directed search (--directed)

Priority-guided BFS that scores states by proximity to potential invariant violations. States that are “closer” to violating an invariant (based on guard and invariant analysis) are explored first. Useful for finding bugs faster in large state spaces.

Swarm verification (--swarm N)

Runs N parallel model checker instances, each with a different random permutation of the action order. Different action orderings explore different parts of the state space first, increasing the chance of finding violations in bounded time. Combines with --max-time for time-bounded bug hunting.

Simulation (specl simulate)

Random trace exploration without exhaustive search. Generates random execution traces by picking enabled actions uniformly at random. Useful for quick sanity checks and understanding spec behavior before committing to full model checking.

Tips and FAQ

General 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 primary 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. If it finds one, re-run without --fast to get the trace.

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

State space scaling guide

Typical sizes:

N=2, small bounds:    ~1K-100K states
N=3, small bounds:    ~100K-10M states
N=4, small bounds:    ~10M-1B states (use --fast)

Common pitfalls

Range expressions in parameters

Range expressions in parameters cannot use arithmetic:

// WRONG
action Act(i: 0..N+1) { ... }

// RIGHT: define a constant
const LIMIT: Int
action Act(i: 0..LIMIT) { ... }

any is boolean, not a binder

any returns true or false. You cannot use the bound variable outside:

// WRONG: v not in scope
let v = any v in 0..N: state[v] == 2 in state[v]

// RIGHT: use fix to bind a value
let v = fix v in 0..N: state[v] == 2

implies precedence in nested quantifiers

Use explicit parentheses:

// Potentially confusing
all i in 0..N: all j in 0..N: A and B implies C

// Clear
all i in 0..N: all j in 0..N: (A and B) implies C

Empty dict type inference

{} is inferred as an empty set, not an empty dict:

// WRONG: type error
var state: Dict[Int, Int]
init { state = {} }

// RIGHT: empty range comprehension
init { state = {i: 0 for i in 1..0} }

No has_key()

Pre-populate all keys and use sentinel values:

init { state = {i: 0 for i in 0..N} }     // 0 = absent
action AddKey(i: 0..N) {
    require state[i] == 0
    state = state | {i: 1}
}

Double assignment

Each variable can only be assigned once per action:

// WRONG
action Bad() { x = 1 and x = 2 }

// Model atomically instead
action Good() { x = 2 }

require after assignment

All require statements must come before any assignments:

// WRONG
action Bad() { x = x + 1 and require y > 0 }

// RIGHT
action Good() { require y > 0; x = x + 1 }

Roadmap

Parsed but not yet in model checker

These features parse and type-check. They will be implemented in the model checker in future releases.

• Temporal operators — always, eventually, leads_to. Compile to IR but blocked at model checking. Will enable liveness verification.
• Fairness declarations — fairness weak Action, fairness strong Action. Parsed but not used by the checker. Required for meaningful liveness checking.
• enabled(Action) and changes(var) — parsed, not evaluated. Will enable stuttering-sensitive properties.

Not yet implemented

• Module composition — EXTENDS / INSTANCE (TLA+-style module imports). Currently each spec is a single module.
• Recursive functions — functions cannot call themselves.

Planned optimizations

• Cranelift JIT — compile guards and effects to native code via Cranelift. Estimated 3-10x additional speedup over the current bytecode VM.
• Swarm verification — N independent search instances with randomized action orderings. Effective for finding bugs in very large state spaces without exhaustive exploration.
• Compiled verifier — SPIN-style approach: generate Rust source code from the spec, compile with rustc, dlopen the result. Maximum performance for production verification runs.