---
license: apache-2.0
base_model: openai/gpt-oss-20b
tags:
- tla-plus
- formal-methods
- model-checking
- rejection-sampling
- rft
- chattla
datasets:
- EricSpencer00/chattla-rft-corpora-v2
language:
- en
pipeline_tag: text-generation
library_name: transformers
---

# ChatTLA v2-sft2 — first verifier-gated RFT checkpoint with holdout passes

gpt-oss-20b fine-tuned on **260 verifier-certified TLA+ generation pairs**
([chattla-rft-corpora-v2](https://hf.co/datasets/EricSpencer00/chattla-rft-corpora-v2)) —
every training example survived a hard-metric gate chain (SANY, TLC model-check,
non-vacuity, mutation battery, decontamination; zero LLM-judge scoring). Targets are
rendered through the gpt-oss **harmony template with final-channel targets** (plain-text
SFT provably breaks gpt-oss channel discipline — that was this project's v2_sft1 lesson).

**Training:** experts-reaching LoRA (r=8, α=16; q/k/v/o_proj + `target_parameters` on
`mlp.experts.gate_up_proj`/`down_proj`, MXFP4 dequantized to bf16), FSDP2, 4 epochs on
260 pairs, loss 2.67→0.52. This is a **full merged bf16 model** (verified: all 48 expert
tensors present).

**Honest evaluation (directional, NOT the project's frozen Gate-2 budget):**
NL→spec generation on a frozen 30-spec holdout, temp 0.8, TLC-verified:
- **pass@4 = 2/30** (specs that base gpt-oss-20b never passes even at pass@32)
- base gpt-oss-20b comparison: pass@1 0/30, pass@32 4/30 (disjoint spec set → capability shift, not sampling luck)
- Known limits: 20B (the project's target is 120B), k=4 vs the frozen k=32 budget; ~23% of samples still fail module extraction.

Part of the prove-TLA project: a verify-until-correct loop (SANY → TLC → non-vacuity →
repair) provides a structural correctness guarantee; the model's job is only to make the
loop converge. This checkpoint is the first evidence that training on the loop's own
survivors transfers capability.