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

A TLA+ specification states a protocol’s behaviour. The distributed computing community uses TLA+ as a tool for finding protocol defects before deployment. Developing specifications requires substantial time and expertise, which motivates AI agents. Current natural-language-to-TLA+ benchmarks accept a module that parses, runs, and satisfies its declared properties. However, a specification can pass all three checks and still describe a different protocol, for example omitting required behaviour, allowing forbidden behaviour, or both. We present EQUINOX, a benchmark for protocol formalisation in TLA+. It contains 115 tasks and scores each output by bounded trace equivalence. Each task uses a published specification as a hidden reference. EQUINOX compares the agent output and this reference in both directions. We benchmark 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 1723 eligible attempts, but only 24.0% reach semantic 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 in 110 further attempts. Together, these results show a capability gap for frontier AI agents on formalising protocols.