Technical Summary: TLA+-Bench

Problem Statement

The field of natural-language to formal specification generation faces a critical measurement gap. While large language models (LLMs) are increasingly tasked with generating TLA+ specifications from natural language descriptions, progress is difficult to quantify accurately. Existing resources typically grade outputs based on textual resemblance to a reference or simple parsing success. These methods fail to verify correctness, often overstating model capability. Unlike general code generation where testing is approximate, TLA+ comes with a decidable oracle (the TLC model checker) that can determine property satisfaction over the full reachable state space. However, prior datasets have not leveraged this exact oracle at scale, nor have they provided the metadata necessary to control for input variations or difficulty levels.

Methodology

Dataset Construction (TLA+-Bench)

The authors constructed a dataset and benchmark comprising 1,300 specifications sourced from 13 public repositories. The dataset is stratified into two tiers:

• Gold Tier (403 specifications): Contains TLA+ modules paired with runnable model-checking configurations. These are verified by the TLC model checker to ensure they satisfy stated properties over the full reachable state space.
• Silver Tier (897 specifications): Contains modules that parse successfully but lack runnable configurations, supporting large-scale parse-rate studies.

Metadata and Augmentation:
Every specification is augmented with:

• Four Natural Language Descriptions: Generated by two providers (GPT-5 and Claude Opus 4.5) in two distinct styles:
  • Declarative: Reveals the module's actual names (testing interface recovery).
  • Intent: Hides names, stating only system requirements (testing design from scratch).
• Labels: Difficulty labels (Basic, Intermediate, Advanced) and category labels (System vs. Utility).
• Trivial Fixture Flagging: Valid specifications with only a single reachable state (which pass trivially) are flagged and excluded from the primary evaluation set to prevent inflated scores.

Evaluation Protocol

The benchmark evaluates models using an execution-grounded approach rather than textual overlap:

1. Validity Gate: The generated specification must parse under the SANY parser.
2. Semantic Gate: The specification is run against the reference configuration using the TLC model checker. TLC explores the full reachable state space to decide if named properties are violated.
3. Correctness Definition: A specification is "correct" only if it passes both gates.

The Correctness Envelope:
The paper introduces the concept of a "correctness envelope" to demonstrate that a single correctness number is insufficient. The authors measure correctness under four distinct regimes on the same set of outputs:

• Configuration-Aware: The model is given the interface names (constants/properties) in the prompt.
• Default: The model must recover interface names from the description alone.
• Substantive: Passes must exercise real behavior (multi-state) and check non-tautological properties.
• Mutation-Surviving: The checked property must be "load-bearing" (verified via mutation testing where the property is replaced with TRUE).

Key Results

1. The Correctness Envelope

The choice of grading regime drastically alters reported performance. On the same set of frontier model outputs:

• Configuration-Aware Rate: 18.7% (Model given interface names).
• Default Rate: 10.0% (Model recovers interface names).
• Substantive Rate: 4.0% (Passes must exercise behavior).
• Mutation-Surviving Rate: 1.7% (Passes must verify non-trivial properties).

This represents an elevenfold difference (18.7% to 1.7%) based solely on grading choices, highlighting that prior benchmarks reporting a single number silently select one of these regimes.

2. Validity vs. Correctness

There is a significant gap between syntactic validity and semantic correctness.

• Frontier Models: Parse rates range from 63% to 89%, but correct rates (under default regime) range from 4% to 16%.
• Open Models: Parse rates are significantly lower (7% to 29%), with correct rates at 0% to 1%.
• Conclusion: Models write valid TLA+ far more often than they write correct TLA+. A benchmark stopping at parsing would falsely rank these models as capable.

3. Difficulty and Failure Modes

• Difficulty Cliff: Correctness drops sharply as problem difficulty increases. For frontier models, the correct rate falls from 25% on basic specifications to 2% on intermediate and advanced specifications.
• Failure Taxonomy: The dominant failure mode is Configuration Binding (mismatched names between the generated module and the reference configuration), accounting for up to 74% of failures for some models. Other failures include parse errors, safety violations, and liveness violations.
• Failure Consistency: Models often fail in the same categories on the same specifications, suggesting the difficulty lies in the task structure as much as the model capability.

Significance and Claims

The paper claims that TLA+-Bench provides the first execution-grounded benchmark for natural-language to TLA+ generation that utilizes an exact oracle. Its primary contribution is not just the dataset, but the methodological insight that an exact oracle does not yield a single correctness number.

Instead, correctness is a range (the "correctness envelope") dependent on:

1. Whether the model is told the interface names.
2. Whether the pass exercises real behavior.
3. Whether the property checked is load-bearing.

The authors assert that previous benchmarks have inflated apparent capability by using weak oracles (e.g., parsing or finite test sets) or by making implicit grading choices. By making these choices explicit and measuring the bounds, TLA+-Bench allows researchers to:

• Measure the true gap between valid and correct generation.
• Study specific failure modes (e.g., interface recovery vs. modeling logic).
• Stratify results by difficulty to understand where models break down.

The paper concludes that while models show promise in generating syntactically valid TLA+, they currently struggle significantly with generating semantically correct specifications, particularly as problem complexity increases or when interface recovery is required. The release includes the specifications, descriptions, model outputs, and grading tools to enable reproducible and extended research.