FuzzTLA

FuzzTLA is work-in-progress on the grant "Hardened Testing of TLA+ Model Checkers" supported by the TLA⁺ Foundation.

The project uses Apalache's Java façade for its TLA+ intermediate representation to synthesize TLA+ specifications.

Tip

This project is under active development. Expect plenty of changes and no backwards compatibility in 2026.

Results

• Conformance reports document corpus-confirmed differences between TLC and Apalache, with counts, classifications, and reduced TLA+ examples.
• Filed findings document confirmed defects in the checked tools, grouped by subsystem and accompanied by reproductions.

Requirements

• JDK 25
• Apache Maven 3.9.10 or newer

Build and test

The Apalache Java façade is a snapshot served by the Central Portal snapshots repository. The build also downloads the pinned Apalache 0.62.2 release archive from GitHub and verifies its SHA-256 digest. Compile and test the project with:

make compile
make test

Build the executable JAR or run all Maven verification checks with:

make package
make verify

Run the command-line application with:

make run
make run ARGS='--help'
make run ARGS='--version'

Once packaged, the launcher can be used directly and from any working directory:

./bin/fuzztla --help
/path/to/model-checker-hardening/bin/fuzztla --version

The launcher runs from a temporary snapshot of the packaged JAR, so a concurrent build cannot replace classes underneath a long-running workflow. It snapshots the staged apalache.jar into the same directory. With no arguments, FuzzTLA prints its help. The executable JAR can also be run without the launcher when it and its sibling target/apalache.jar will not be rebuilt during the invocation:

java -jar target/fuzztla.jar --help

Commands

Initialize a corpus in the default corpus directory with:

./bin/fuzztla init

Use --corpus to select another directory. Initialization creates this layout without overwriting an existing configuration:

corpus/
├── config.toml
├── 00-inputs/
├── 01parser-pass/
├── 01parser-fail/
├── 01parser-crash/
├── 02tlc-inputs/
├── 02tlc-pass/
├── 02tlc-counterexample/
├── 02tlc-fail/
├── 02tlc-crash/
├── 02apa-inputs/
├── 02apa-pass/
├── 02apa-counterexample/
├── 02apa-fail/
├── 02apa-crash/
├── 03aggregator-pass/
└── 03aggregator-fail/

The initialized configuration below assumes eight available processors. The Apalache worker count is computed from the processors visible to the JVM.

[generator]
max_type_depth = 3
max_expression_depth = 32
max_nodes = 32
max_collection_size = 8
max_string_bytes = 32
max_integer_bytes = 16
ignore = ["action", "temporal", "unbound", "exotic"]
weights = { name = 8, enum_set = 16 }
classpath = []
custom_operators = []

[workflow]
# Maximum number of unique entries across every workflow directory.
max_entries = 1000

[workflow.inputs]
# Maximum current occupancy of 00-inputs.
max_entries = 1000

[workflow.parser]
# Maximum combined occupancy of the parser result directories.
max_entries = 1000
# Wall-clock limit for parsing one generated specification.
timeout_sec = 30

[workflow.tlc]
# Maximum combined occupancy of the TLC result directories.
max_entries = 1000
# Wall-clock limit for checking one generated specification.
timeout_sec = 30
# Maximum heap allocated to each isolated TLC JVM.
max_heap_mb = 512
# Number of TLC model-checking workers in each isolated JVM.
workers = 1

[workflow.apalache]
# Maximum combined occupancy of the Apalache result directories.
max_entries = 1000
# Wall-clock limit for checking one generated specification.
timeout_sec = 30
# Maximum heap allocated to each persistent Apalache worker JVM.
max_heap_mb = 1024
# Number of concurrent FuzzTLA Apalache workers.
# Initialized to half the available processors, rounded down (at least one).
workers = 4

[pbt]
# Inclusive upper bound on a randomly generated input's length.
max_input_bytes = 10240
# Number of uniformly selected collection-richness cohorts.
richness_cohorts = 10
# Weight multiplier for each level of collection-literal nesting.
richness_nesting_base = 2.0
# Base of the geometric minimum-richness schedule.
richness_threshold_base = 1.5

Every generated expression form has one category. generator.ignore excludes the selected categories, the structural types that require them, and forms that depend on their syntax. The available excludable categories are action, temporal, unbound, exotic, control, label, operator, quantifier, bool_logic, arithmetic, set, finite_set, universe, sequence, function, fold, tuple, record, variant, and model. The reserved core category supplies atomic leaves and terminal fallback and cannot be ignored. generator.weights accepts the lowercase name of every ExpressionKind implementation, such as plus, fold_set, or temporal_forall. Unlisted kinds have weight one.

Dependencies are disabled transitively. For example, ignoring set also removes bounded quantifiers and function values because they require set-valued domains. Set ignore = [] to enable every excludable category. The fixed workflow module still uses Next == UNCHANGED exprValue; filtering applies to the expression copied into Init and Inv. The current format requires every listed field and workflow directory.

Custom TLA+ operators

Custom operators are additional kinds, not replacements for standard operators. For example, put this module in <corpus>/tla/MyOperators.tla:

---- MODULE MyOperators ----
Singleton(value) == {value}
Contains(values, value) == value \\in values
====

Set these fields in the existing [generator] table:

classpath = ["./tla"]
custom_operators = [
  { module = "MyOperators", operators = ["Singleton", "Contains"] },
]
weights = { name = 8, enum_set = 16, "MyOperators!Contains" = 8 }

Names are case-sensitive TLA+ identifiers. Paths are relative to config.toml; directories and JARs are searched in order. A JAR may contain Module.tla at its root or under tla2sany/StandardModules/. Standard module overrides and Java operator overrides are not supported.

FuzzTLA runs the pinned Apalache CLI's typecheck --infer-poly=true --output once per module before generation. Inferred types and ordinary @type annotations are supported, including polymorphic record/variant rows. Each generated call instantiates its signature independently. Only selected operators become kinds; helpers are linked automatically. Exclusions apply to the complete helper closure, and each unweighted custom kind has weight one.

Definitions must be first-order and state-free: no operator-valued parameters or results, free constants/variables, assumptions, recursive definitions, or action/temporal constructs. Types must be representable by the generator; real, legacy record, sparse-tuple and empty record/variant/tuple types are unsupported. Library source snapshots are bounded to 32 MiB, typed JSON to 64 MiB, and each preparation process uses the Apalache stage's heap and timeout limits.

Both checker formats are self-contained, and standalone expression printing uses LET for library definitions. The first run records .operator-library in an empty corpus, pinning source contents, selected operators and the Apalache JAR. Subsequent runs and print --corpus reject mismatches. Keep the same sources to replay inputs; initialize a new corpus when changing a library. No subprocess is launched for library preparation when custom_operators = [].

Running

Populate the corpus with property-based inputs by running:

./bin/fuzztla run --how=pbt
./bin/fuzztla run --how=pbt --corpus=another-corpus --seed=42 --max-cpus=4

The command runs input generation, parsing, TLC, Apalache, and conformance aggregation concurrently. Generation and parsing maintain up to --max-cpus workers; parser workers use persistent isolated JVMs. Each TLC input runs in a fresh JVM. A TLC process uses workflow.tlc.workers internal workers and reserves that many permits from the shared downstream-priority CPU budget, so at most floor(max-cpus / workflow.tlc.workers) TLC processes run concurrently. The TLC worker count must not exceed --max-cpus. Each FuzzTLA Apalache worker lazily starts one isolated JVM and calls Tool.run sequentially for multiple inputs. Workers run concurrently and reserve one permit per active call. A timeout or crash retires the child JVM, and the next input starts a replacement. The initialized worker count is half the available processors, rounded down with a minimum of one; the stored setting also must not exceed --max-cpus. The aggregator has priority over TLC and Apalache, which have equal checker priority over parsing, which has priority over generation. Waiting checker requests reserve partial CPU capacity so upstream work cannot starve them. Before starting, FuzzTLA validates the corpus, recovers interrupted moves, completes partial parser fan-outs, reconstructs ready checker pairs, and finishes interrupted aggregate source deletion.

When standard output is an interactive ANSI terminal, run refreshes its progress table in place once per second. Redirected output omits intermediate updates. After all stage workers stop, the table changes to FINALIZING while FuzzTLA validates the complete corpus for the final summary.

The workflow tries random byte arrays until workflow.max_entries unique accepted inputs exist across all directories. Lengths are selected from uniformly chosen logarithmic buckets—0..3, 4..7, 8..15, and so on through max_input_bytes—and uniformly within the selected bucket.

For each missing corpus entry, the input stage uniformly selects one richness cohort. Cohort 0 accepts every generated expression. Cohort c > 0 requires a collection-richness score of at least richness_threshold_base^(c - 1). The score sums the size of every explicit set, sequence, tuple, and record literal, weighted by richness_nesting_base for each enclosing collection literal. With the default configuration, the ten effective integer cutoffs are 0, 1, 2, 3, 4, 6, 8, 12, 18, 26.

The selected cohort remains fixed while generator rejections, insufficiently rich expressions, and duplicate inputs are retried. A failure to fill one cohort after 10,000 candidates stops the workflow with the cohort, threshold, and best score in the diagnostic. The progress table reports candidate attempts, generator rejections, richness rejections, and duplicates separately. It also reports the minimum, maximum, and average richness of inputs admitted during the current run. Stage progress distinguishes inputs awaiting the parser, TLC, Apalache, and aggregation and reports verdict counters for every stage.

The effective nonnegative seed is printed and flushed before corpus access or worker startup. The input stage derives a stable seed for each generator worker, which owns independent cohort and candidate streams. Reusing the main seed, configuration, starting corpus, and --max-cpus reproduces those worker-local streams. Dynamic target claiming, duplicate races, and parser-capacity timing may still change the aggregate corpus. Every stored raw input remains exactly replayable. Entries begin in 00-inputs/<sha256>.cbor; its compact gen field records the selected cohort and admission-time richness score. The parser preserves this metadata, records tagged UTC timestamps and a verdict, and moves the entry to its parser result directory. Parser passes are copied to 02tlc-inputs and 02apa-inputs; the two files count as one logical corpus entry. TLC records stages.tlc and moves its copy to the matching TLC result directory. Apalache does the same under stages.apalache and its result directories. Once both non-crash results exist, the aggregator merges their metadata into one entry. Equal pass/pass, counterexample/counterexample, or fail/fail verdicts move to 03aggregator-pass; any disagreement, including a counterexample from only one checker, moves to 03aggregator-fail. Failure codes do not affect this comparison. A pair with a checker crash remains in the checker result directories. The parser and TLC receive a TLA+ module; Apalache receives typed Apalache IR JSON generated from the same expression. The JSON path preserves closed expression types that TLA+ source cannot fully annotate. Both checkers run the fixed Init, Next, and Inv configuration with deadlock checking disabled. Apalache uses the artifact's exploration length, which is zero for an expression input. A property violation is a counterexample; classified evaluation, typechecking, and parsing errors are failures. Both stages use the shared failure-code taxonomy for failures.

Among generator exceptions, only InputRejectedException rejects a candidate; other failures stop the workflow. An unexpected generator or parser-preparation failure preserves the exact input and stack trace under .work/generator-crash/<sha256>.{cbor,stacktrace} and reports the artifact path. These diagnostic files do not count as corpus entries. A crashed parser writes 01parser-crash/<sha256>.stacktrace with the exception stack trace or other crash diagnostic.

A crashed checker invocation similarly writes 02tlc-crash/<sha256>.stacktrace or 02apa-crash/<sha256>.stacktrace. Parser and checker temporary files live under <corpus>/.work/{parser,tlc,apalache}-tmp and are removed after the run.

Install the triager's Python dependency and classify crash diagnostics and conformance aggregator failures with:

python3 -m pip install -r script/requirements.txt
python3 script/triager.py corpus

The triager writes 01parser-crash-triage.csv, 02tlc-crash-triage.csv, 02apa-crash-triage.csv, and 03aggregator-fail-triage.csv in the corpus directory. Each row contains the entry hash and either the matching finding or conformance-report filename, or NEW. Signatures are conservative and deterministic: add one only after confirming that the diagnostic has the same root cause as the named document. Aggregator signatures also require the documented checker verdict pair and failure code; ambiguous diagnostics and unmatched counterexample pairings remain NEW. The Corpus triage workflow runs a short, fixed-seed fuzzing session and publishes these CSV files as a workflow artifact.

Generate a deterministic, typed TLA+ expression from a CBOR corpus input with:

./bin/fuzztla print input.cbor
./bin/fuzztla print --corpus=corpus corpus/00-inputs/example.cbor
./bin/fuzztla print --envelope --corpus=corpus corpus/02apa-inputs/example.cbor
./bin/fuzztla print --spec --corpus=corpus corpus/01parser-crash/example.cbor
./bin/fuzztla print --apalache-ir --corpus=corpus corpus/02apa-crash/example.cbor

print always expects the CBOR envelope described above. By default, it prints the generated expression. --spec prints the TLA+ specification passed to the parser and TLC. --apalache-ir prints the normalized typed JSON passed to Apalache. --envelope prints the supported envelope fields as a nested, human-readable listing. These output modes are mutually exclusive. Stage timestamps use UTC ISO-8601, and each endTime includes the elapsed time since its startTime. The input field appears last, rendered as TLA+. Without --corpus, the command uses the built-in generator defaults. With --corpus, it uses the generator settings in that corpus's config.toml, which is necessary to replay inputs under changed generator settings.

kind: expr
gen:
  cohort: 7
  richness: 18.0
stages:
  parser:
    verdict: pass
    startTime: 2026-08-13T14:26:07Z
    endTime: 2026-08-13T14:27:30Z (duration: 1m 23s)
input:
  FALSE

The embedded input byte string is interpreted directly by FuzzTLA's generator framework. Variable-length values use per-element continuation markers—an odd byte continues and an even byte terminates—instead of a length prefix. The encoding is implementation-local and may change between versions; a suffix may remain unused when the selected expression is complete.

License

Licensed under either of

• Apache License, Version 2.0 (LICENSE-APACHE), or
• MIT License (LICENSE-MIT).