EQUINOX: Benchmarking Natural-Language-to-TLA+ Formalisation by Bounded Trace Equivalence

A TLA+ specification describes a protocol's behaviour. The distributed computing community uses TLA+ to find protocol defects before deployment. Writing these specifications requires substantial time and expertise, which motivates the use of AI agents. Current natural-language-to-TLA+ benchmarks accept a specification that parses, runs, and satisfies its declared properties. However, a specification can pass all three checks yet describe a different protocol by omitting required behaviour, allowing extra behaviour, or both. We present EQUINOX, a benchmark for protocol formalisation in TLA+. It contains 115 tasks and evaluates each output using bounded trace equivalence. Each task uses a published specification as a hidden reference. EQUINOX compares the behaviours of the agent output and the hidden reference in both directions. We evaluate five agents: Codex + GPT-5.6 Sol, Codex + GPT-5.6 Terra, Claude Code + Opus 5, Claude Code + Sonnet 5, and OpenCode + GLM-5.3. We report three results. First, execution is necessary but not sufficient for successful formalisation. Nontrivial execution accepts 73.0% of the 1723 eligible attempts, but only 24.0% satisfy bounded trace equivalence. Second, the agents solve similar sets of tasks: no agent solves 71 of 115 tasks, while all five agents solve 24 tasks. Third, more attempts rarely resolve modelling errors. Codex + GPT-5.6 Sol solves 1 of 11 selected failed tasks across 110 further attempts. Together, these results show a capability gap for frontier AI agents in protocol formalisation.