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
cargo install --path crates/specl-cli
specl check examples/other/Counter.specl -c MAX=5module 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 }
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.
| Raft consensus | Leader election + log replication (Vanlightly's async model) |
| Percolator | Google's distributed transactions with snapshot isolation |
| CometBFT | Tendermint BFT with Byzantine faults |
| Paxos | Single-decree Paxos (Synod) consensus |
| MESI | Cache coherence protocol |
| Redlock | Distributed lock bug-finding (Kleppmann attack) |
See examples/showcase/ for curated protocol specs, examples/other/ for additional specs.
- VSCode extension — diagnostics, hover, completion, format-on-save (Marketplace)
- Formatter —
specl format spec.specl --write - Watch mode —
specl watch spec.specl -c N=3 - TLA+ translator —
specl translate spec.tla -o spec.specl
Specl includes an expert skill for Claude Code that teaches Claude how to write, debug, and verify Specl specifications.
Option 1: Load as plugin (recommended for easy updates)
claude --plugin-dir /path/to/speclSkills will be namespaced: /specl:expert-specl
Option 2: Install skill only (lightweight)
./install-skill.shSkills will be available without namespace: /expert-specl
Claude will automatically use the skill when you:
- Work with
.speclfiles - 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
cargo test --workspace && cargo clippy --workspacePolyForm Noncommercial 1.0.0 — free for non-commercial use. See commercial licensing for commercial use. Contact [email protected].