Crate tla_connect 

tla-connect: TLA+/Apalache integration for model-based testing.

Provides three complementary approaches for connecting TLA+ formal specifications to Rust implementations:

1. Approach 1 (Apalache -> ITF -> replay): Batch trace generation + replay. Apalache generates ITF traces from TLA+ specs, which are replayed against a Rust Driver. Direct equivalent of the Quint/quint-connect workflow. Requires features: replay, trace-gen.

2. Approach 2 (Apalache JSON-RPC): Interactive symbolic testing. Step-by-step symbolic execution via Apalache’s explorer server, interleaved with Rust implementation execution. Requires feature: rpc.

3. Approach 3 (Rust -> NDJSON -> Apalache): Post-hoc trace validation. Record Rust execution traces as NDJSON, then validate against a TLA+ TraceSpec using Apalache. Requires feature: trace-validation.

Approaches 1 & 2 catch “implementation doesn’t handle a case the spec allows.” Approach 3 catches “implementation does something the spec doesn’t allow.”

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

Quick Start (Approach 1)

use tla_connect::*;

#[derive(Debug, PartialEq, Deserialize)]
struct MyState { /* TLA+ vars to compare */ }

impl State for MyState {}

impl ExtractState<MyDriver> for MyState {
    fn from_driver(driver: &MyDriver) -> Result<Self, DriverError> { /* ... */ }
}

struct MyDriver { /* Rust type under test */ }

impl Driver for MyDriver {
    type State = MyState;
    fn step(&mut self, step: &Step) -> Result<(), DriverError> {
        switch!(step {
            "init" => { /* init */ Ok(()) },
            "action1" => { /* ... */ Ok(()) },
        })
    }
}

let traces = generate_traces(&ApalacheConfig {
    spec: "../../formal/tla/MySpec.tla".into(),
    ..Default::default()
})?;
replay_traces(|| MyDriver::default(), &traces.traces)?;

Re-exports

pub use driver::debug_diff;

pub use driver::Driver;

pub use driver::ExtractState;

pub use driver::State;

pub use driver::Step;

pub use error::BuilderError;

pub use error::DriverError;

pub use error::Error;

pub use error::TlaResult;

pub use error::ApalacheError;

pub use error::DirectoryReadError;

pub use error::ReplayError;

pub use error::TraceGenError;

pub use error::ValidationError;

pub use error::StepContext;

pub use error::StepError;

pub use replay::replay_trace_str;

pub use replay::replay_traces;

pub use replay::replay_traces_with_progress;

pub use replay::ReplayProgress;

pub use replay::ReplayProgressFn;

pub use replay::ReplayStats;

pub use trace_gen::generate_traces;

pub use trace_gen::ApalacheConfig;

pub use trace_gen::ApalacheConfigBuilder;

pub use trace_gen::ApalacheMode;

pub use trace_gen::GeneratedTraces;

pub use trace_validation::validate_trace;

pub use trace_validation::StateEmitter;

pub use trace_validation::TraceResult;

pub use trace_validation::TraceValidatorConfig;

pub use trace_validation::TraceValidatorConfigBuilder;

Modules

driver

Core abstractions for connecting Rust implementations to TLA+ specs.

error

Typed errors for tla-connect.

replay

ITF trace replay runner (Approach 1).

trace_gen

Apalache trace generation (Approach 1).

trace_validation

Trace validation: record Rust execution traces and validate against TLA+ specs using Apalache (Approach 3).

Macros

switch

Dispatch a TLA+ action to the corresponding Rust code.