expert-specl

name: expert-specl description: > Expert for Specl, a modern specification language and model checker for concurrent and distributed systems. Covers the full Specl language, CLI toolchain, distributed protocols (Raft, Paxos, consensus, BFT), concurrent algorithms, and formal verification. Use when: writing/debugging .specl files, modeling distributed systems, verifying safety properties, analyzing invariant violations, optimizing state space exploration, or translating TLA+. Keywords: specl, model checking, formal verification, TLA+, distributed systems, consensus, Raft, Paxos, BFT, invariants, state space, specification language.

Specl — Specification Language & Model Checker

Specl is an exhaustive model checker for concurrent and distributed systems. Write a spec (state machine), and the checker explores every reachable state to verify invariants or produce minimal counterexample traces.

Modern TLA+ alternative with clean syntax, implicit frame semantics, and a fast Rust engine (1M+ states/second).

Quick Reference

Installation

# From Specl repo at /Users/danwt/Documents/repos/specl/specl
cargo install --path crates/specl-cli    # `specl` binary
cargo install --path crates/specl-lsp    # language server (optional)

VSCode extension: https://marketplace.visualstudio.com/items?itemName=specl.specl

Essential Commands

specl check spec.specl -c N=3 -c MAX=10    # check with constants
specl check spec.specl --no-deadlock        # skip deadlock check (for protocols)
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 fmt spec.specl --write                # auto-format
specl fmt spec.specl --lint                # fast syntax + type + compile check
specl info spec.specl -c N=3              # state space analysis + estimates
specl watch spec.specl -c N=3              # re-check on save
specl translate spec.tla -o spec.specl     # TLA+ to Specl
specl check spec.tla -c N=3               # auto-translate TLA+ and check

Minimal Example

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 }

Run: specl check Counter.specl -c MAX=3 → explores all 4 states, verifies invariant.

Critical Language Rules

• = assigns next-state (in actions). == compares (in guards/invariants).
• Variables not mentioned in an action stay unchanged (implicit frame — no UNCHANGED needed).
• Use and to update multiple variables atomically in one action.
• require is a guard/precondition. If false, action is skipped (not an error).
• Checker explores ALL actions × ALL parameter combinations × ALL reachable states via BFS.
• ALL require statements MUST come BEFORE any assignments in an action.

Language Reference

Module Structure

module Name

const C: Int              // set at check time: -c C=5
var x: 0..10              // state variable with type bound

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

action Step() { ... }     // state transition

func Helper(a) { ... }    // pure function (no state modification)

invariant Safe { ... }    // must hold in every reachable state

Types

Operators

Dicts (The Workhorse)

Model N processes with state via dicts. Create with comprehension, update with | (merge):

var role: Dict[Int, Int]
init { role = {p: 0 for p in 0..N} }
action Promote(i: 0..N) { role = role | {i: 2} }

Multi-key update:

balance = balance | { from: balance[from] - amt, to: balance[to] + amt }

Nested dict update (e.g., votesGranted[i][j]):

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

Empty dict initialization (avoid type inference error):

// ❌ WRONG: {} is inferred as Set
var state: Dict[Int, Int]
init { state = {} }  // Type error!

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

Parameterized Actions

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

Quantifiers

all x in 0..N: P(x)       // universal: true if P holds for ALL x
any x in 0..N: P(x)       // existential: true if P holds for SOME x

Work in invariants, guards, and any expression.

Set Comprehensions

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

Functions

Pure, no state modification, used for reusable logic:

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

Common Modeling Patterns

Process Ensemble

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

Message Passing

Encode messages as sequences (tuples), store in a set:

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

// Message format: [type, src, dst, payload...]
action Send(src: 0..N, dst: 0..N, term: Int) {
    require role[src] == CANDIDATE
    msgs = msgs union {[1, src, dst, term]}  // RequestVote
}

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

Quorum Checking

// Simple majority (2f+1 out of N)
len({v in 0..N if votes[v]}) * 2 > N + 1

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

Encoding Enums

Use integer constants with comments:

// Roles: 0=Follower, 1=Candidate, 2=Leader
var role: Dict[Int, 0..2]
action BecomeCandidate(i: 0..N) {
    require role[i] == 0  // Follower
    role = role | {i: 1}  // → Candidate
}

Multiple Variable Updates

Use and to update multiple variables atomically:

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

Modelling Approach

1. Identify state. What variables fully describe the system? For N processes, use Dict[Int, ...].
2. Identify actions. What transitions can happen? Use parameters for nondeterminism.
3. Write guards. require restricts when actions fire.
4. Write invariants. Safety properties that must always hold.
5. Start small. Use N=2 or N=3, small bounds. State spaces grow exponentially.

CLI Flags Reference

Analyzing Results

OK Result

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 (unless --no-deadlock).

Invariant Violation

Result: INVARIANT VIOLATION
  Invariant: Consistency
  Trace (5 steps):
    0: init
    1: BecomeCandidate(i=0)
    2: RequestVote(src=0, dst=1)
    3: GrantVote(src=1, dst=0)
    ...

How to debug:

1. Read trace step-by-step (each step = one action + resulting state)
2. Identify which action caused violation
3. Check if guards are too weak (action shouldn't have fired)
4. Check if invariant is too strict (async timing issues)

Deadlock

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

A reachable state where no action is enabled. For protocols this is often expected (use --no-deadlock). For liveness/progress properties, reveals real bugs.

Common Pitfalls & Solutions

Performance Optimization

State Space Estimation

Factors:

• Number of processes: Exponential impact (N=2 → N=3 can be 100× larger)
• Value ranges: Multiplicative (0..10 vs 0..5)
• Message sets: Combinatorial explosion
• Dict sizes: Cartesian product of all key-value combinations

State space orders of magnitude:

• 10-100 states: Tiny (Counter, simple locks)
• 100-10K states: Small (basic protocols, small N)
• 10K-100K states: Medium (realistic protocols with N=2)
• 100K-1M states: Large (use --fast)
• 1M+ states: Very large (use --fast + --por + --symmetry)

Reduction Techniques

1. Smaller constants: N=2 instead of N=3 (100× reduction)
2. Tighter types: 0..3 instead of Int
3. Bounded collections: require len(msgs) < 10
4. Abstraction: Model at right level (don't model implementation details)
5. Symmetry reduction: --symmetry flag (all processes identical)
6. Partial order reduction: --por flag (independent actions)
7. Fast mode: --fast (8 bytes/state, no traces)

Optimization Workflow

# 1. Start small, verify correctness
specl check spec.specl -c N=2 -c MaxTerm=1

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

# 3. Add partial order reduction if needed
specl check spec.specl -c N=2 -c MaxTerm=2 --por

# 4. Use fast mode for large spaces
specl check spec.specl -c N=3 -c MaxTerm=2 --por --fast

# 5. Add symmetry if applicable
specl check spec.specl -c N=3 -c MaxTerm=2 --por --symmetry --fast

TLA+ Comparison

Key advantages over TLA+:

• Cleaner syntax (no backslash operators)
• Implicit frame semantics (no UNCHANGED)
• Faster model checker (Rust vs Java)
• Better type inference
• Integrated toolchain (formatter, LSP, watch mode)

Examples Repository

Location: /Users/danwt/Documents/repos/specl/specl/examples/

Showcase (examples/showcase/)

Curated protocol specs reviewed for faithfulness and invariant coverage:

• raft.specl — Raft consensus (async, Vanlightly model)
• paxos.specl — Single-decree Paxos (Synod)
• comet.specl — CometBFT/Tendermint BFT with Byzantine faults
• simplex.specl — Simplex consensus (TCC 2023)
• percolator.specl — Google Percolator (snapshot isolation)
• mesi.specl — MESI cache coherence
• redlock.specl — Redis Redlock bug-finding (Kleppmann attack)
• swim.specl — SWIM failure detection
• chandy-lamport.specl — Consistent snapshot algorithm
• TwoPhaseCommit.specl — Classic 2PC
• narwhal_tusk.specl — Narwhal/Tusk DAG consensus (design reference)

Other (examples/other/)

Additional specs: beginner examples, semaphore puzzles (prefixed sem-), stress tests, simplified protocol models, and more.

Use Cases

✅ Good Fit

• Distributed consensus protocols (Raft, Paxos, Byzantine agreement)
• Distributed transactions (2PC, snapshot isolation, serializable isolation)
• Byzantine fault tolerance (PBFT, BFT consensus)
• Concurrent algorithms (locks, semaphores, barriers, queues)
• Safety property verification (mutual exclusion, consistency, linearizability)
• Cache coherence protocols (MESI, MOESI)
• Network protocols (alternating bit, sliding window)
• Finding minimal counterexamples (shortest path to violation)
• Small-to-medium state spaces (< 10M states, or larger with --fast)

❌ Not a Good Fit

• Liveness properties (fairness, eventual consistency) — TLA+ with fairness better suited
• Infinite state spaces without abstraction — use theorem proving (Coq, Isabelle)
• Performance modeling — use simulation or queueing theory
• Smart contract logic — use Solidity analyzers (Slither, Mythril)
• Real-time systems — use timed automata (UPPAAL)
• Probabilistic systems — use PRISM or Storm
• Very large state spaces without reduction techniques (>100M states)

Key Insights

Why Specl Over TLA+?

• Cleaner syntax — no backslash operators, implicit frame
• Faster checker — Rust vs Java, 1M+ states/second
• Better tooling — formatter, LSP, watch mode, integrated translator
• Better type inference — less type annotation needed
• Lower barrier to entry — simpler syntax, clearer error messages

When to Use Model Checking

• Finding bugs in protocols — exhaustive search finds corner cases
• Verifying safety properties — proves invariants hold in all reachable states
• Understanding protocol behavior — traces show actual execution paths
• Bounded verification — proves correctness within bounds (term, log length, etc.)

Limitations

• State space explosion — exponential growth with N processes
• Bounded model checking — correctness proven only within bounds
• No liveness — can't prove "eventually" properties (use TLA+ with fairness)
• Abstraction required — must model at right level (not too detailed)

Project Structure

/Users/danwt/Documents/repos/specl/specl/
├── crates/
│   ├── specl-syntax/   # Lexer, parser, AST, pretty-printer
│   ├── specl-types/    # Type checker
│   ├── specl-ir/       # IR, bytecode compiler, guard indexing
│   ├── specl-eval/     # Tree-walk evaluator + bytecode VM
│   ├── specl-mc/       # BFS explorer, parallel via rayon, state store
│   ├── specl-tla/      # TLA+ parser and translator
│   ├── specl-cli/      # CLI (the `specl` binary)
│   └── specl-lsp/      # Language server
├── examples/
│   ├── easy/           # 12 beginner examples
│   ├── realistic/      # 16 mid-complexity examples
│   └── benchmark/      # 18 production protocols
└── editors/            # VSCode extension

/Users/danwt/Documents/repos/specl/examples/
├── semaphores/         # 13 semaphore puzzles
└── realistic/          # narwhal_tusk.specl

Resources

• Specl repo: /Users/danwt/Documents/repos/specl
• Main examples: /Users/danwt/Documents/repos/specl/specl/examples/
• Semaphore puzzles: examples/other/sem-*.specl
• VSCode extension: https://marketplace.visualstudio.com/items?itemName=specl.specl
• Manual: https://danieltisdall.com/specl
• Announcement: https://danieltisdall.com/blog/2026-02-11-0028