LoRA adapter for openai/gpt-oss-120b, trained on the W4 "diamond-gold" corpus of verifier-accepted TLA+ specifications (~5,010 surviving examples, 517 with liveness properties).

The merged full-weight model is at chattla-w4dg-120b — see that card for the full evaluation, including the caveats, which apply equally here.

For vLLM serving, prefer the pre-merged chattla-w4dg-120b.

Frozen 30-spec holdout, pass@32, scored by SANY + TLC:

No comparison against the previous checkpoint is statistically significant (McNemar exact p = 0.22 vs. 11/30). A control group of 17 identical-prompt specs showed spec-level verdicts moving by one and row-level counts swinging much harder across runs, so single-run pass@32 at k=32 should not be read as a capability signal without multiple seeds.

Only ~2% of framing-A attempts fail because the system was modeled incorrectly; the rest fail mechanically (parse errors, missing EXTENDS, name collisions). Budget for a repair loop.

Research on LLM-assisted formal specification. Output is a candidate module, meaningful only once SANY/TLC accepts it — not a source of verified specs on its own.

Project repo: https://github.com/LUC-AI4FM/tla-prover