Specl

A specification language and model checker for concurrent and distributed systems. Modern alternative to TLA+/TLC: clean syntax, implicit frame semantics, fast Rust engine.

Full manual | Announcement | VSCode Extension

Quick start

cargo install --path specl/crates/specl-cli
specl check specl/examples/other/Counter.specl -c MAX=5

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 }

A spec defines a state machine: const values are fixed at check time (-c N=3), var declarations are the mutable state the checker tracks, init sets the starting state, action blocks are transitions (guarded by require), and invariant blocks are safety properties that must hold in every reachable state. Variables not mentioned in an action stay unchanged (implicit frame). = assigns, == compares.

Performance

Faster than TLC (the standard TLA+ model checker) on all benchmarks tested. Written in Rust with a bytecode VM, incremental fingerprinting, guard indexing, and parallel BFS.

With parallelism: 1M+ states/second on typical workloads.

Examples

Peterson	Mutual exclusion for 2 processes
Dining Philosophers	Classic concurrency problem
Two-Phase Commit	Distributed transaction protocol
G-Counter	Grow-only counter CRDT
MESI	Cache coherence protocol
Paxos	Single-decree Paxos (Synod) consensus
Redlock	Distributed lock bug-finding (Kleppmann attack)
Raft	Leader election + log replication (Vanlightly's async model)

See examples/ for the full catalogue (100+ specs) and verification results.

Toolchain

• VSCode extension — diagnostics, hover, completion, rename, format-on-save (Marketplace)
• Formatter — specl fmt spec.specl --write (also: --check for CI, --lint for full compile check)
• Spec analysis — specl info spec.specl -c N=3 (state space breakdown, time/memory estimates, optimization tips)
• Watch mode — specl watch spec.specl -c N=3
• TLA+ translator — specl translate spec.tla -o spec.specl (or specl check spec.tla to auto-translate and check)

Claude Code Integration

Specl includes an expert skill for Claude Code that teaches Claude how to write, debug, and verify Specl specifications.

Installation

Option 1: Load as plugin (recommended for easy updates)

claude --plugin-dir /path/to/specl

Skills will be namespaced: /specl:expert-specl

Option 2: Install skill only (lightweight)

./install-skill.sh

Skills will be available without namespace: /expert-specl

Usage

Claude will automatically use the skill when you:

• Work with .specl files
• Ask about model checking or formal verification
• Mention distributed protocols (Raft, Paxos, 2PC, etc.)
• Debug invariant violations or deadlocks

Or invoke it directly:

/expert-specl help me model a consensus protocol

Development

cargo test --workspace --exclude specl-tla
cargo test -p specl-tla --test translate_corpus -- --skip benchmark_tla_files_translate
cargo clippy --workspace

(The TLA+ translator uses deep recursion that overflows the 8MB default stack in unoptimized debug builds. CI and release builds are not affected.)

License

PolyForm Noncommercial 1.0.0 — free for non-commercial use. See commercial licensing for commercial use. Contact contact@danwt.com.