gpt-oss-120b fine-tuned on the W4 "diamond-gold" corpus of TLA+ specifications (rejection-sampling fine-tune; ~5,010 verifier-surviving examples, 517 with liveness properties). Weights are the merged LoRA; the adapter alone is at chattla-w4dg-120b-adapter.

This is a research checkpoint from an ongoing project on getting guaranteed-correct TLA+ out of a verify loop rather than out of the weights. Please read the evaluation section before drawing conclusions from it.

Evaluation — read this before using the numbers

Evaluated on a frozen 30-spec holdout at pass@32 (k=32, temperature 0.8), scored by SANY + TLC against each spec's reference .cfg.

arm	task	result
framing A	generate a whole spec from a natural-language description	16/30
framing B	repair a corrupted spec	partial run, ~52% row-level pass

None of the differences between this checkpoint and its predecessor are statistically significant.

comparison	McNemar exact (2-sided)
vs. previous checkpoint (11/30)	p = 0.22
before vs. after a harness fix (15/30 → 16/30)	p = 1.000

During this evaluation, 17 of the 30 specs had byte-identical prompts across two runs, forming an accidental control group. Spec-level verdicts moved by one, and row-level pass counts swung considerably more (one spec went 5 → 1 passes, another 7 → 12) on identical inputs. The practical consequence:

Single-run per-spec pass@32 at k=32 is not a reliable capability signal for this benchmark. Treat any single-run comparison — including the ones above — as inconclusive without multiple seeds.

What the failures are made of

Across 990 framing-A attempts:

outcome	share
`sany=fail` (does not parse / semantic errors)	67.7%
`tlc=error` (config or runtime)	14.7%
pass	13.6%
genuine semantic failures (invariant / liveness / deadlock violated)	~2%

Only about 2% of attempts fail because the model modeled the system incorrectly. The rest are mechanical: undeclared identifiers, missing EXTENDS, name collisions with standard-module operators, duplicate definitions. Anyone using this model should expect a repair or lint pass to matter more than sampling more candidates.

A benchmark defect found during this evaluation

Part of the measured failure rate was the harness, not the model. The evaluation prompt was built from each spec's reference .cfg, but a parser bug discarded the right-hand side of substitution entries (Nat <- NatOverride), so the prompt asked for Nat and never mentioned NatOverride — while TLC hard-fails without it. That affected 13 of the 30 holdout specs.

After fixing it, one spec went from 0/33 to 8/33 and another flipped, but ten of the thirteen stayed at zero — the prompt defect was hiding further independent blockers. The fix and analysis are in the project repo.

Intended use

Research on LLM-assisted formal specification: generating candidate TLA+ modules to be checked by SANY/TLC, and repairing broken ones.

Not suitable for producing verified specifications unsupervised. Model output is a candidate and is only meaningful once a model checker has accepted it. The project this checkpoint comes from treats the verifier, not the weights, as the source of correctness.

Limitations

Framing-A output frequently fails to parse (~68%); budget for a repair loop.
Weakest on specs needing an MC-wrapper idiom (finitizing Nat or Seq via a .cfg substitution) — it will often define the override operator incorrectly, e.g. {0 .. MaxNat-1} (a set of sets) instead of 0 .. MaxNat.
Repair (framing B) is substantially stronger than generation from scratch. On two specs where framing A scores 0/33, framing B scores 29/33 and 9/11.
Holdout is 30 specs. Small denominators, wide error bars.

Training

Base: openai/gpt-oss-120b
Method: rejection-sampling fine-tune — candidates generated, kept only if SANY + TLC accepted them against a reference .cfg
Corpus: W4 "diamond-gold", ~5,010 surviving examples (517 with liveness)
Hardware: ALCF Sophia, 8×A100 80GB
Serving used for eval: vLLM TP=8, --max-model-len 32768

Citation

bibtex

@misc{spencer2026chattla_w4dg,
  title  = {chattla-w4dg-120b: rejection-sampling fine-tuning for TLA+ specification synthesis},
  author = {Spencer, Eric},
  year   = {2026},
  url    = {https://huggingface.co/EricSpencer00/chattla-w4dg-120b}
}