Software and Datasets¶
AI4FM develops its research artifacts in the open. Our source code lives under the LUC-AI4FM GitHub organization, and the trained models and corpora produced by that code are published on Hugging Face - available for reuse and replication.
Note
This page lists our publicly released repositories. Work that is still under submission or embargo is released once the associated paper is public.
Models and Fine-Tuning¶
TLA-Prove (ChatTLA)
The training and evaluation code behind TLA-Prover,
published at ICSOFT 2026. The distinguishing choice is the training metric: success
is measured by whether a generated specification passes the TLC model checker, not
by perplexity. The resulting 20B model is derived from openai/gpt-oss-20b and
released under Apache 2.0.
ralph-tla
Experiments pairing the Ralph specification language with TLA+ in a self-correcting loop: the model drafts a specification, SANY and TLC check it, and the resulting errors are fed back to the model until the specification passes. A test of whether verifier feedback can substitute for human repair.
Released Models¶
The ChatTLA model family, fine-tuned from openai/gpt-oss base models for TLA+
specification synthesis. All are released under Apache 2.0 and are
published on Hugging Face.
Model |
Size |
Description |
|---|---|---|
20B |
The model behind TLA-Prover (ICSOFT 2026), trained with supervised fine-tuning and GRPO. A GGUF build is available for local inference via Ollama and llama.cpp. |
|
20B |
Retrained on the verifier-gated RFT corpus below, so every training example is one the model checker already accepted. |
|
117B |
The largest model in the family, fine-tuned on the W4 diamond/gold corpus. Also published as a LoRA adapter for use on top of the stock base model. |
|
20B (LoRA) |
Targets TLAPS proof construction rather than specification generation - the harder downstream task of proving a spec’s invariants. |
Released Datasets¶
Training and evaluation corpora produced by the pipelines above. These are verifier-gated: examples are kept only if SANY parses them and TLC accepts them, so the corpora contain machine-checked specifications rather than merely plausible ones.
Dataset |
Size |
Description |
|---|---|---|
4,119 rows |
Diamond- and gold-tier survivors of a cross-family verify-until-correct loop, exported as SFT text. The largest corpus in the set. |
|
1K-10K rows |
Rejection-sampling fine-tuning (RFT/STaR) corpus for specification generation.
Used to train |
|
1,125 SFT rows |
Training and evaluation corpora for the TLAPS theorem-proving work. |
|
Artifact |
A reproducible TLAPS proof artifact recording a 108/108 prover result. |
Data Pipelines and Evaluation¶
tla-dataset-pipeline
A pipeline that discovers TLA+ repositories across GitHub, extracts .tla,
.cfg, and .tlaps files, parses them with LLM-based analysis, and archives
the results to S3. Discovery runs nightly under CI with DVC-tracked state, so the
corpus grows continuously rather than being frozen at collection time.
TLA+-Bench
The execution-grounded benchmark and dataset behind our natural-language-to-TLA+ research. Its public reviewer release includes 1,300 specifications, a reproducible grader, and 403 TLC-model-checked gold specifications.
TLAKit
TLA+ tools for Python, Jupyter notebooks, and CI. TLAKit uses the official TLA+ tools to run checks, inspect counterexamples, and work with specifications from a notebook or command line.
Generation Pipelines¶
TLA+ Specification Generator
A hosted research prototype for generating a TLA+ specification from a system description. Returned candidates are checked with SANY and TLC before being surfaced for review. An access key is required to generate specifications.
FormaLLM
A research pipeline for generating TLA+ specifications from natural language, orchestrated with ZenML and backed by OpenAI, Anthropic, or local Ollama models. Separates prompting, parsing, and evaluation into swappable pipeline steps so that backends and prompting strategies can be compared under identical conditions.
paper-parse
Tooling for extracting structured data from research PDFs at scale, used to build the comment-ratio dataset supporting our empirical software engineering work.
Contributing¶
Our repositories are open to students and collaborators. If you are interested in working on any of these projects, see Get Involved.