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. 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

The tla-ts command takes TLC's options and prints TLC's output. tla-ts prove takes tlapm's options and prints tlapm's output.

Check a spec

To check a spec, pass its path:

npx tla-ts Spec.tla

tla-ts reads the configuration from Spec.cfg next to the spec. It exits with the exit code TLC uses for the same result.

You can pass several paths, or a glob such as "specs/*.tla". tla-ts checks each spec in turn and exits with the exit code of the first spec that fails. A glob skips each module that has no .cfg next to it, so it doesn't check helper modules that other specs import. tla-ts never skips a path that you pass by name. If you pass a .cfg path, tla-ts checks the .tla file with the same name.

The options are:

• -config : read the configuration from this file. You can use it only when you check one spec.
• -deadlock: don't report deadlocks.
• -dump [dot[,colorize][,actionlabels][,snapshot]] : write every reachable state to .dump, or with dot, the state graph to .dot. The output matches TLC run with -fp 0. tla-ts doesn't support the constrained, stuttering, or strict formats.
• -lncheck final: check liveness once, after the search ends.
• -seed : seed RandomElement and the Randomization module. The default is 0.
• -workers : search with this number of worker threads. auto uses one thread per core. The default is 1.

Generate proof obligations

A proof obligation is one claim that a backend prover must prove. tla-ts prove -N prints the obligations of a module, as tlapm -N does. It doesn't run a prover. For example, this command prints every obligation in Module.tla with its text:

npx tla-ts prove -N --toolbox 0 0 --printallobs Module.tla

With --toolbox or --line, tla-ts writes the messages of the TLA+ Toolbox protocol to stderr, as tlapm does. If you pass a tlapm option that isn't in this list, tla-ts prints an error:

• --toolbox : print Toolbox messages for the proofs from line start to line end. 0 0 selects the whole module.
• --line : print Toolbox messages for the proof at this line.
• --printallobs: print the text of each obligation.
• --summary: print the number of obligations in each module, and list its missing and omitted proofs. You don't need -N with --summary.
• --strict: report missing proofs, omitted proofs and a selected range with no obligations as errors.
• -I : search this directory for modules.

1. The directory of each module you pass, the last one first.
2. The current directory.
3. The standard library of tlapm, which has the TLAPS module. tla-ts searches it only if tlapm is on your PATH.
4. The -I directories, the last one first.

Prove with tlapm

tla-ts doesn't include a prover. Without -N or --summary, tla-ts prove runs tlapm from your PATH:

npx tla-ts prove Module.tla

tla-ts expands the globs and passes every argument to tlapm, so all of tlapm's options work. tlapm sends the obligations to its provers, and tla-ts exits with the exit code of tlapm. If tlapm isn't on your PATH, tla-ts prints an error and exits with code 1.

API reference

check

Checks a spec against a TLC configuration and resolves to the result.

import { check } from "tla-ts";
const result = await check({
  source: specSource,
  config: configSource,
  loadModule: (name) => modules[name],
  onPrint: (text) => console.log(text),
});

| Option | Description | | ----------------------- | ---------------------------------------------------------------------------------------- | | source | The TLA+ module to check | | config | A TLC configuration, as text or as the result of parseConfig | | loadModule | Returns the source of a module that isn't a standard module | | loadClass | Returns a compiled Java class that overrides a module's operators with constants | | onPrint | Receives the output of Print and PrintT. Defaults to console.log | | onPause | Runs when TLCSet("pause", TRUE) pauses checking, which resumes when it returns | | readFile, writeFile | Read and write files for the Json module and dump | | seed | A bigint seed. Defaults to 0n, and matches TLC run with the same -seed and -fp 0 | | workers | The number of worker threads. Defaults to 1 | | dump | Writes the reachable states or the state graph, as TLC's -dump does |

dump takes the path that check passes to writeFile before it returns. Set dot to write the state graph in the DOT language of Graphviz, and colorize, actionLabels, or snapshot for TLC's formats of the same names. A dump checks the spec on the calling thread, as one TLC worker does.

The result has these fields:

• status: "success", "deadlock", "assumption-violation", "invariant-violation", "property-violation", "liveness-violation", "postcondition-violation", or "error".
• violation: the name of what failed and the trace that reaches it. loopStart marks where a liveness counterexample loops back.
• failure: the message and trace when status is "error".
• generatedStates, distinctStates, and depth: TLC's state counts.

• SharedArrayBuffer is unavailable, as on a page without cross-origin isolation.
• The spec has liveness properties.
• The spec uses impure operators such as Print.
• The configuration has VIEW, POSTCONDITION, or _POSSIBLE.

check supports:

• Modules: the standard modules, TLCExt, Json, and Randomization, plus EXTENDS, INSTANCE, and LAMBDA.
• Configuration: CONSTANTS, INIT, NEXT, SPECIFICATION, invariants, properties, constraints, SYMMETRY, VIEW, ALIAS, POSTCONDITION, CHECK_DEADLOCK, and _POSSIBLE.
• Properties: invariants and every temporal formula TLC accepts, checked through TLC's tableau construction.
• TLC semantics: 32-bit integer overflow, TLCGet and TLCSet, subexpression references such as Op!2, and TLC's enumeration order for CHOOSE and quantifiers.

parseModule

Parses a TLA+ module into its syntax tree. Throws TlaSyntaxError on invalid input.

import { parseModule } from "tla-ts";
const module = parseModule(specSource);
module.name; // "Counter"

parseConfig

Parses a TLC configuration file into a ModelConfig. Pass the result to check to change it before checking.

import { check, parseConfig } from "tla-ts";
const config = parseConfig(configSource);
config.checkDeadlock = false;
await check({ source: specSource, config });

formatValue

Prints a value in TLA+ syntax, as TLC prints it in traces.

import { formatValue } from "tla-ts";
result.violation?.trace.forEach((step) => {
  Object.entries(step.state).forEach(([name, value]) => console.log(name, formatValue(value)));
});

Errors

Every error extends TlaError:

• TlaSyntaxError: the module does not parse
• TlaConfigError: the configuration is invalid or refers to an unknown name
• TlaEvaluationError: evaluation failed, as when TLC reports an error
• TlaUnsupportedError: the spec uses a feature tla-ts does not support yet

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

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