Rejection-sampling fine-tuning (RFT/STaR) corpus for TLA+ specification generation,
produced by the prove-TLA verify-until-correct loop (2026-07-10/11). Every survivor
passed the full hard-metric gate chain — no LLM-judge scoring anywhere:
SANY parse → semantic-invariant cfg gate → TLC model-check (non-vacuous, ≥3 distinct
states) → NL↔invariant linkage contract (PROPERTY_INVARIANT named, defined, checked… See the full description on the dataset page:
https://huggingface.co/datasets/EricSpencer00/chattla-rft-corpora-v2.
