Skip to content

FuzzTLA

FuzzTLA tests the TLA+ model checkers TLC and Apalache. It generates random TLA+ specifications, checks each one with both tools, and keeps every specification on which they disagree, fail or crash. A campaign therefore finds defects in either checker and documents where their semantics differ.

Under active development

Input and output formats, configuration keys and corpus layouts may change without notice. Initialize a new corpus after upgrading FuzzTLA.

How it works

flowchart LR
  G[Generate] --> P[Parse with SANY]
  P --> T[TLC]
  P --> A[Apalache]
  T --> C[Compare verdicts]
  A --> C
  C --> Q[Select inputs for mutation]
  Q -. next generation .-> G
  1. Generate. FuzzTLA turns random bytes into a well-typed TLA+ module. The same bytes always produce the same module.
  2. Parse. SANY, the TLA+ parser, must accept the module.
  3. Check. TLC and Apalache check the module with the same Init, Next and invariant, independently and in parallel.
  4. Compare. If the verdicts differ, for example a pass against a counterexample, the entry is a disagreement.
  5. Select and mutate. Agreeing entries that exercise the checkers well seed the next generation of inputs.

Every input, verdict and diagnostic is stored in a corpus, a directory you can resume, inspect, query and report on.

Where to start