Instructions to use EricSpencer00/chattla-w4dg-120b with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use EricSpencer00/chattla-w4dg-120b with Transformers:

# Use a pipeline as a high-level helper
from transformers import pipeline

pipe = pipeline("text-generation", model="EricSpencer00/chattla-w4dg-120b")
messages = [
    {"role": "user", "content": "Who are you?"},
]
pipe(messages)

# Load model directly
from transformers import AutoTokenizer, AutoModelForCausalLM

tokenizer = AutoTokenizer.from_pretrained("EricSpencer00/chattla-w4dg-120b")
model = AutoModelForCausalLM.from_pretrained("EricSpencer00/chattla-w4dg-120b", device_map="auto")
messages = [
    {"role": "user", "content": "Who are you?"},
]
inputs = tokenizer.apply_chat_template(
	messages,
	add_generation_prompt=True,
	tokenize=True,
	return_dict=True,
	return_tensors="pt",
).to(model.device)

outputs = model.generate(**inputs, max_new_tokens=40)
print(tokenizer.decode(outputs[0][inputs["input_ids"].shape[-1]:]))

Notebooks
Google Colab
Kaggle
Local Apps Settings

vLLM

How to use EricSpencer00/chattla-w4dg-120b with vLLM:

Install from pip and serve model

# Install vLLM from pip:
pip install vllm
# Start the vLLM server:
vllm serve "EricSpencer00/chattla-w4dg-120b"
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:8000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "EricSpencer00/chattla-w4dg-120b",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker

docker model run hf.co/EricSpencer00/chattla-w4dg-120b

SGLang

How to use EricSpencer00/chattla-w4dg-120b with SGLang:

Install from pip and serve model

# Install SGLang from pip:
pip install sglang
# Start the SGLang server:
python3 -m sglang.launch_server \
    --model-path "EricSpencer00/chattla-w4dg-120b" \
    --host 0.0.0.0 \
    --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "EricSpencer00/chattla-w4dg-120b",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Use Docker images

docker run --gpus all \
    --shm-size 32g \
    -p 30000:30000 \
    -v ~/.cache/huggingface:/root/.cache/huggingface \
    --env "HF_TOKEN=<secret>" \
    --ipc=host \
    lmsysorg/sglang:latest \
    python3 -m sglang.launch_server \
        --model-path "EricSpencer00/chattla-w4dg-120b" \
        --host 0.0.0.0 \
        --port 30000
# Call the server using curl (OpenAI-compatible API):
curl -X POST "http://localhost:30000/v1/chat/completions" \
	-H "Content-Type: application/json" \
	--data '{
		"model": "EricSpencer00/chattla-w4dg-120b",
		"messages": [
			{
				"role": "user",
				"content": "What is the capital of France?"
			}
		]
	}'

Docker Model Runner
How to use EricSpencer00/chattla-w4dg-120b with Docker Model Runner:
```
docker model run hf.co/EricSpencer00/chattla-w4dg-120b
```

chattla-w4dg-120b

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

@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}
}

Downloads last month: 34

Safetensors

Model size

117B params

Tensor type

BF16

Model tree for EricSpencer00/chattla-w4dg-120b

Base model

openai/gpt-oss-120b

Finetuned

(107)

this model