Tlaiser

TLAiser extracts state machine specifications from existing code and model-checks them with TLA+/PlusCal — catching concurrency bugs that no amount of testing finds.

TLA+ (Temporal Logic of Actions, by Leslie Lamport) is the gold standard for specifying and verifying concurrent and distributed systems. PlusCal is its imperative-style front-end that compiles to TLA+. The TLC model checker exhaustively explores all possible states to find invariant violations and liveness failures.

Amazon, Microsoft, and Intel use TLA+ internally to verify distributed systems. TLAiser brings this power to everyone — you describe your system, TLAiser generates the spec and runs the checker.

TLAiser leverages the full power of TLA+ temporal logic:

• □ (Always) — safety properties: "bad things never happen" (e.g., no deadlock, no data corruption, mutual exclusion holds)

• ◇ (Eventually) — liveness properties: "good things eventually happen" (e.g., every request gets a response, every lock is eventually released)

• ↝ (Leads-to) — temporal ordering: "if A happens, B eventually follows" (e.g., if a message is sent, it is eventually delivered)

• Fairness conditions — weak/strong fairness constraints that prevent unrealistic infinite stuttering of enabled actions

• Catch distributed systems bugs before production — deadlocks, race conditions, protocol violations, split-brain scenarios

• Exhaustive verification — TLC checks ALL possible interleavings, not just the ones your tests happen to exercise

• Counterexample traces — when a violation is found, TLAiser shows exactly the sequence of steps that triggers the bug

• Safety + Liveness — verify both that bad things never happen AND that good things eventually do

• Distributed protocol verification — Raft, Paxos, 2PC, custom consensus

• Database transaction isolation — verify serialisability, snapshot isolation, read-committed guarantees under concurrent transactions

• Consensus algorithm validation — prove agreement, validity, and termination properties before implementation

• Microservice choreography checking — verify saga patterns, event-driven workflows, and distributed state machines for deadlock-freedom

• Lock-free data structure verification — prove linearisability of concurrent algorithms

Describe your system’s state transitions in tlaiser.toml. TLAiser:

1. Extracts state machine models from your code (or from the manifest)

2. Generates TLA+ specifications with safety and liveness properties

3. Runs the TLC model checker to exhaustively verify all reachable states

4. Reports violations with concrete counterexample traces

Follows the hyperpolymath -iser pattern (same as Chapeliser):

• Manifest (tlaiser.toml) — describe WHAT you want to verify

• Idris2 ABI (src/interface/abi/) — formal proofs: state machine types, temporal formulae, model check results all verified at compile time

• Zig FFI (src/interface/ffi/) — C-ABI bridge to TLC runtime and state extraction engine

• Codegen (src/codegen/) — generates TLA+/PlusCal specifications from extracted state machines

• Rust CLI — parses manifest, extracts state machines, generates specs, invokes TLC, reports results

User writes zero TLA+. TLAiser generates everything.

Part of the -iser family of acceleration frameworks.

Pre-alpha. Architecture defined, scaffolding in place, codegen pending.

SPDX-License-Identifier: PMPL-1.0-or-later