Tlaiser

Table of Contents

• What Is This?
• Pipeline
• TLA+ Concepts
• Key Value
• Use Cases
• How It Works
• Architecture
• Quick Start
• Status
• License

What Is This?

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.

Pipeline

Source Code                TLA+ Spec              TLC Model Checker
    │                         │                        │
    ▼                         ▼                        ▼
┌──────────┐  extract   ┌──────────┐  generate  ┌──────────┐
│ Your code │ ────────► │  State   │ ────────► │  TLA+/   │
│ or TOML   │           │ Machine  │           │ PlusCal  │
│ manifest  │           │  Model   │           │   Spec   │
└──────────┘            └──────────┘           └──────────┘
                                                     │
                                                     ▼ model-check
                                               ┌──────────┐
                                               │   TLC    │
                                               │ Checker  │
                                               └──────────┘
                                                     │
                                                     ▼
                                               ┌──────────┐
                                               │ Invariant│
                                               │ Violation│
                                               │  Report  │
                                               └──────────┘

TLA+ Concepts

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

Key Value

• 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

Use Cases

• 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

How It Works

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

# tlaiser.toml — example: distributed lock service
[workload]
name = "distributed-lock"
entry = "src/lock_service.rs::LockStateMachine"
strategy = "state-extraction"

[data]
input-type = "LockRequest"
output-type = "LockGrant | LockDenied | LockTimeout"

[properties]
safety = ["MutualExclusion", "NoDeadlock"]
liveness = ["EventualAccess"]
fairness = "weak"

[model]
processes = 3
max-steps = 50

Architecture

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.

Quick Start

# Initialise a manifest in your project
tlaiser init

# Edit tlaiser.toml to describe your state machine

# Generate TLA+ specs and run TLC
tlaiser generate
tlaiser run

# Or all at once
tlaiser build && tlaiser run

Status

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

License

SPDX-License-Identifier: CC-BY-SA-4.0