Eric Spencer
projects
This is the dataset release from the ChatTLA+ work on training models to generate TLA+ specifications. The TLA-Prover paper at ICSOFT 2026 describes the training and evaluation. The GitHub repository keeps its anonymized review-era name and README, but the corpus and benchmark are public.
The dataset has two parts. The first is corpus/diamond_sft.jsonl, 209 rows of supervised fine-tuning data. Each row is an OpenAI-style chat list (developer, user, assistant) in which the assistant turn is a TLA+ spec that TLC validated. Every row carries semantic metadata: how many distinct states TLC explored, what fraction of declared actions were exercised, whether the spec caught at least one mutation of its invariant, and how many invariants were checked. The _source: opus_subagent tag records that an Opus-family model drafted the seed and TLC verified it, which is a methodology marker rather than an author hint.
The second part is a 30-problem held-out benchmark in benchmark/, split across six domains: consensus and election, data structures, classical puzzles, scheduling and resources, transactions and databases, and workflows and state machines. There are five problems per domain. Each entry has a natural-language description, an ordinal 1-5 difficulty, the invariants the spec must declare, and a module-name pointer to the closest reference spec in the public tlaplus/examples repository. No verbatim files from tlaplus/examples are redistributed, only pointers, which keeps the licensing clean. The dataset itself is CC-BY-4.0.
A small eval.jsonl of four prompts is used as a generation eval during training.
The TLA-Prove training repository holds the validator, training, and evaluation code. The chattla-20b model card describes the model release. Use the paper's evaluation procedure when comparing results; a model card or a later checkpoint can describe a different run.
The 209-row ChatTLA+ dataset is separate from TLA+-Bench, the later 1,300-specification benchmark. TLA+-Bench has its own dataset, grader, and recorded model outputs. For smaller examples of what TLC checks, see the TLA+ project guide.