tla-ts

tla-ts is a drop-in replacement for TLC that's 2× faster.

TLA+ lets you write formal models of a system, and TLC model checks them. But TLC is written in Java and needs the JVM. tla-ts runs anywhere JavaScript runs, such as the browser, Node, and Bun. tla-ts also checks TLAPS proofs, so you can write proofs and check them without tlapm. Try it in the playground.

import { check } from "tla-ts";

const result = await check({
  source: `---- MODULE Counter ----
EXTENDS Naturals
VARIABLE x
Init == x = 0
Next == x' = x + 1
Small == x < 3
====`,
  config: "INIT Init NEXT Next INVARIANT Small",
});

result.status; // "invariant-violation"

Install

npm install tla-ts

Command line

npx tla-ts Spec.tla          # check a spec with TLC's options
npx tla-ts bank.ts           # compile TypeScript to TLA+ and check it
npx tla-ts tlapm Module.tla  # tlapm's command line, with tla-ts's provers

Check TypeScript

tla-ts compiles a TypeScript file to a TLA+ spec and config, writes them beside the file, and checks them. Variables become state, exported functions that change state become actions, and exported functions that return a boolean become invariants.

// bank.ts
type Account = "alice" | "bob";

let balances: Record<Account, number> = { alice: 10, bob: 10 };

export const transfer = (from: Account, to: Account, amount: 1 | 2 | 3) => {
  balances[from] -= amount;
  balances[to] += amount;
};

export const noOverdraft = () => balances.alice >= 0 && balances.bob >= 0;

npx tla-ts bank.ts writes Bank.tla and Bank.cfg, and reports that noOverdraft is violated after four transfers from bob. Check TypeScript lists every construct tla-ts compiles.

API

check

const result = await check({ source, config });
result.status; // "success", "deadlock", "invariant-violation", ...
result.violation?.trace;

Option	Description
source	The TLA+ module
config	A TLC configuration
loadModule	Returns the source of an imported module
workers	The number of worker threads. Defaults to 1

A check with several workers starts over on one worker when it orders two strings that the search created, such as with \o or ToString. This happens when both strings go into one set or one function's domain. TLC orders strings by when it first sees them, and workers share that order only for strings that exist before the search. The CLI prints a warning when this happens, and check passes onProgress a sequential-fallback event.

prove

const result = await prove({ source });
result.obligations; // each with a status: "proved", "trivial", "failed", or "unsupported"

Option	Description
source	The TLA+ module
loadModule	Returns the source of an imported module
onObligation	Receives each obligation as soon as it's decided
workers	The number of worker threads. Defaults to 1

parseModule

const module = parseModule(source);
module.name; // "Spec"
module.definitions;

parseConfig

const config = parseConfig(configSource);
config.invariants.push("TypeOK");
await check({ source, config });

formatValue

const step = result.violation.trace[0];
formatValue(step.state.queue); // "<<1, 2>>"

Errors

Error	Thrown when
TlaError	Any of the errors below
TlaSyntaxError	The module doesn't parse
TlaConfigError	The configuration is invalid
TlaEvaluationError	Evaluating the spec fails
TlaUnsupportedError	The spec or call uses something tla-ts can't do

Benchmarks

Wall time on one worker, including JVM and Node startup. Both checkers report the same state counts on every model.

Spec	Distinct states	TLC	tla-ts	Speedup
Two-phase commit	282,251	4.32 s	2.01 s	2.2×
Dining philosophers	128,889	1.06 s	0.71 s	1.5×
Bounded queue	44,044	0.37 s	0.17 s	2.2×
542 conformance models		986.6 s	403.3 s	2.4×

Wall time on 8 workers, also including startup. Each time is the median of 3 runs on an Apple M4 Pro.

Spec	Distinct states	TLC	tla-ts	Speedup
Raft with reconfiguration	298,493	10.50 s	8.96 s	1.2×
Sailfish	109,604	4.34 s	4.07 s	1.1×
Fast Paxos	25,617	3.91 s	2.57 s	1.5×
Buffered random access file	3,316	4.70 s	3.61 s	1.3×

Development

pnpm install
pnpm test
pnpm dev

pnpm dev starts the playground in packages/website.

Run the conformance suite against TLC's recorded results:

pnpm --filter tla-ts conformance:fetch
pnpm --filter tla-ts conformance

Run the TLC and tlapm conformance suites in packages/conformance:

pnpm --filter @tla-ts/conformance fetch-tlc
pnpm --filter @tla-ts/conformance fetch-tlapm
pnpm --filter @tla-ts/conformance conformance

Rerun the benchmarks with TLA2TOOLS_JAR set to the path of tla2tools.jar:

pnpm --filter tla-ts bench
pnpm --filter tla-ts bench:corpus

License

MIT