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

Type	Example	Notes
Bool	true, false
Int	42, -7	Unbounded
Nat	0, 100	Non-negative
0..10		Inclusive range of ints
Set[T]	{1, 2, 3}	Finite set
Seq[T]	[a, b, c]	Ordered list (0-indexed)
Dict[K, V]	{k: 0 for k in 0..N}	Map from keys to values
String	"red"	String literal

Operators

Category	Operators
Logical	and, or, not, implies, iff
Comparison	==, !=, <, <=, >, >=
Arithmetic	+, -, *, /, %
Set	in, not in, union, intersect, diff, subset_of
Sequence	++ (concat), head(s), tail(s), len(s), s[i] (index)
Conditional	if ... then ... else ... (expression — always requires else)

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

Flag	Effect	When to Use
-c KEY=VAL	Set constant value	Always (e.g., -c N=3 -c MaxTerm=2)
--no-deadlock	Don't report deadlocks	Protocols with quiescent states (most distributed protocols)
--fast	Fingerprint-only (no traces, 8 bytes/state)	Large state spaces (>1M states), or when memory-constrained
--por	Partial order reduction	Independent processes/actions (e.g., message passing)
--symmetry	Symmetry reduction	Identical processes (homogeneous systems)
--no-parallel	Single-threaded	Debugging, deterministic output
--threads N	Set thread count	Fine-tune parallelism
--max-states N	Stop after N states	Testing, time limits
--max-depth N	Limit exploration depth	Bounded verification
--memory-limit N	Max memory in MB	Resource limits
--write	(format) Write in place	Auto-formatting

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

Pitfall	Solution
= vs == confusion	= assigns in actions, == compares in invariants/guards
Empty dict {} type error	Use {i: 0 for i in 1..0} for empty dict
require after assignment	ALL requires must come before ANY assignments
No has_key() function	Pre-populate dict with all keys, use dict[k] == val
State space explosion	Start with N=2, reduce ranges, use --fast/--por/--symmetry
Deadlock on protocol spec	Add --no-deadlock (quiescent states are expected)
Range with arithmetic in param	Can't use 0..N+1, define const MAX instead
any used as binder	any x: P(x) is Bool, can't use x outside
Double assignment to variable	Model critical section atomically, don't acquire + release
Invariant fails due to async timing	Relax invariant or check fundamental property only

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

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

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