← Back to blog

Specl: a faster TLA+ for the rest of us

speclformal-verificationmodel-checkingdistributed-systems

I've been building Specl, a specification language and model checker for concurrent and distributed systems. It's a modern replacement for TLA+/TLC. It's AI friendly too.

Why?

TLA+ is brilliant for verifying distributed systems, but the tooling hasn't kept up. The syntax is cryptic (/\, \/, \A, \E, EXCEPT). The model checker (TLC) is Java from 2002. There's no formatter, no language server, no modern editor integration.

Specl fixes all of that:

module Counter

const MAX: 0..10
var count: 0..10

init {
    count = 0
}

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

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

No primed variables. No UNCHANGED. No /\. Just = for assignment, == for comparison, and/or/not for logic. Variables you don't mention stay unchanged automatically.

Performance

The model checker is written in Rust and is faster than TLC on every benchmark I've tested. With parallelism enabled, Specl can hit 1M+ states/second.

Under the hood: bytecode VM for guards and effects, incremental invariant checking with bitmasks, guard indexing, operation caching, partial order reduction, and parallel BFS via rayon.

Toolchain

It's not just a checker. There's a full toolchain:

  • VSCode extension with syntax highlighting, real-time diagnostics, hover, completion, and format-on-save
  • Formatter (specl format --write)
  • Watch mode (specl watch spec.specl -c N=3) — re-checks on every save
  • TLA+ translator (specl translate spec.tla) — converts existing TLA+ specs

What it's verified

The repo includes Specl specifications for Raft, Paxos, EPaxos, Multi-Paxos, Two-Phase Commit, Percolator, Parallel Commits, Dining Philosophers, PBFT, and MESI cache coherence — all with verified identical state counts against TLC.

Try it

git clone https://github.com/danwt/specl.git
cd specl/specl
cargo install --path crates/specl-cli
specl check examples/easy/Counter.specl -c MAX=5

Full guide and language reference: Specl Guide

GitHub: danwt/specl