TLA+ Bench

This dataset contains structured JSON extractions from 206 TLA+ formal specification files drawn from the TLA+ Examples repository. Each specification is processed using a multi-stage language model pipeline that identifies and labels syntactic and semantic features of TLA+ modules, including operator definitions, action definitions, temporal properties, fairness conditions, proof constructs, and PlusCal content. Extraction versions. Each specification includes three JSON files: Base Extraction from the raw TLA+ source using a language model Fine-grained Extraction extends the base version with a four-way classification of operator definitions (StatePredicate, TemporalProperty, Init, ValueDef) and additional subcategories such as function constructors and UNCHANGED expressions AST Extraction derived from the SANY parse tree and used for comparison with the language model outputs Schema. Each JSON record contains fields describing module structure, operator and variable names, logical and set operators, temporal and fairness constructs, proof elements, PlusCal content, and a natural language description of the specification. A complete field-by-field codebook is included. Intended use. This dataset is intended for training and evaluating language models on formal specification tasks, supporting corpus analysis of TLA+ code, and enabling research on automated extraction of semantic information from formal methods artifacts.