tla-connect

TLA+/Apalache integration for model-based testing in Rust.

Overview

tla-connect provides tools for integrating TLA+ and Apalache model checking into Rust test suites. It enables:

• Trace validation: Verify that your implementation matches TLA+ specifications
• Model-based testing: Generate test cases from TLA+ models
• Counterexample replay: Automatically reproduce bugs found by model checkers

Architecture

flowchart TB
    subgraph TLA["TLA+ Specification"]
        Spec[MySpec.tla]
        TraceSpec[TraceSpec.tla]
    end

    subgraph Apalache["Apalache Model Checker"]
        CLI[apalache-mc CLI]
        RPC[JSON-RPC Server]
    end

    subgraph Rust["Rust Implementation"]
        Driver[Driver trait]
        State[State trait]
        Emitter[StateEmitter]
    end

    subgraph Traces["Trace Formats"]
        ITF[ITF Traces]
        NDJSON[NDJSON Trace]
    end

    %% Approach 1: Batch Replay
    Spec -->|"generate_traces()"| CLI
    CLI -->|produces| ITF
    ITF -->|"replay_traces()"| Driver
    Driver -->|compared via| State

    %% Approach 2: Interactive RPC  
    Spec -->|"interactive_test()"| RPC
    RPC <-->|step-by-step| Driver

    %% Approach 3: Post-hoc Validation
    Driver -->|records| Emitter
    Emitter -->|writes| NDJSON
    NDJSON -->|"validate_trace()"| CLI
    CLI -->|checks against| TraceSpec

    classDef tla fill:#e1f5fe,stroke:#01579b
    classDef apalache fill:#fff3e0,stroke:#e65100
    classDef rust fill:#e8f5e9,stroke:#2e7d32
    classDef trace fill:#fce4ec,stroke:#880e4f

    class Spec,TraceSpec tla
    class CLI,RPC apalache
    class Driver,State,Emitter rust
    class ITF,NDJSON trace

Features

• ITF (Informal Trace Format) parsing and validation
• Apalache CLI integration for trace generation
• Apalache JSON-RPC client for interactive symbolic testing
• Trace generation from TLA+ specifications
• State comparison and diff output for debugging mismatches
• Support for both file-based and RPC-based workflows

Feature Flags

• replay (default): ITF trace replay against a Driver
• trace-gen (default): Apalache CLI trace generation
• trace-validation (default): Post-hoc NDJSON trace validation
• rpc: Interactive symbolic testing via Apalache JSON-RPC
• parallel: Parallel trace replay using rayon
• full: Enable all features

Installation

Add this to your Cargo.toml:

[dependencies]
tla-connect = "0.0.2"

# For interactive RPC testing:
# tla-connect = { version = "0.0.2", features = ["rpc"] }

Quick Start

Approach 1: Batch Trace Replay

Generate traces with Apalache, then replay against your implementation:

use tla_connect::*;
use serde::Deserialize;

#[derive(Debug, PartialEq, Deserialize)]
struct MyState {
    counter: i64,
}

impl State<MyDriver> for MyState {
    fn from_driver(driver: &MyDriver) -> Result<Self, DriverError> {
        Ok(MyState { counter: driver.counter })
    }
}

struct MyDriver {
    counter: i64,
}

impl Driver for MyDriver {
    type State = MyState;

    fn step(&mut self, step: &Step) -> Result<(), DriverError> {
        switch!(step {
            "init" => { self.counter = 0; },
            "increment" => { self.counter += 1; },
            "decrement" => { self.counter -= 1; },
        })
    }
}

fn main() -> Result<(), Error> {
    let config = ApalacheConfig::builder()
        .spec("specs/Counter.tla")
        .inv("TraceComplete")
        .build();

    let generated = generate_traces(&config)?;
    replay_traces(|| MyDriver { counter: 0 }, &generated.traces)?;
    Ok(())
}

Approach 2: Interactive Symbolic Testing (requires rpc feature)

Step-by-step symbolic execution via Apalache's explorer server:

use tla_connect::*;

#[tokio::main]
async fn main() -> Result<(), Error> {
    let client = ApalacheRpcClient::new("http://localhost:8822").await?;

    let config = InteractiveConfig::builder()
        .spec("specs/Counter.tla")
        .num_runs(100)
        .max_steps(50)
        .seed(42) // Reproducible runs
        .build();

    interactive_test(|| MyDriver::default(), &client, &config).await?;

    Ok(())
}

Approach 3: Post-hoc Trace Validation

Record your implementation's execution, then validate against the spec:

use tla_connect::*;
use serde::Serialize;
use std::path::Path;

#[derive(Serialize)]
struct RecordedState {
    counter: i64,
}

fn main() -> Result<(), Error> {
    // Record execution trace
    let mut emitter = StateEmitter::new(Path::new("trace.ndjson"))?;
    emitter.emit("init", &RecordedState { counter: 0 })?;
    emitter.emit("increment", &RecordedState { counter: 1 })?;
    emitter.emit("increment", &RecordedState { counter: 2 })?;
    emitter.finish()?;

    // Validate against TLA+ spec
    let config = TraceValidatorConfig::builder()
        .trace_spec("specs/CounterTrace.tla")
        .build();

    let result = validate_trace(&config, Path::new("trace.ndjson"))?;

    match result {
        TraceResult::Valid => println!("Trace is valid!"),
        TraceResult::Invalid { reason } => println!("Invalid: {reason}"),
    }

    Ok(())
}

Requirements

• Rust 1.93 or later
• Apalache (if using trace generation or validation features)

Documentation

For detailed documentation, see docs.rs/tla-connect.

License

Licensed under either of:

• Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.