Can LLMs Model Real Systems in TLA+

The Specula team released SysMoBench, putting several LLMs including Claude, GPT, Gemini, DeepSeek, Kimi, and Qwen to the task of modeling real systems in TLA+.

The benchmark evaluates 11 systems across 4 stages: syntax, runtime, conformance, invariant. Syntax and executability were generally high, but a large performance gap opened up in matching actual code behavior and in safety/liveness invariants.

There are two core failure patterns.

• Following textbook-style templates and creating unreachable states
• Merging code that is split across multiple steps into a single atomic action, thereby missing states that are actually possible

For example, in ZooKeeper FLE, mistakes appeared such as modeling recvset as a set union instead of a map, or bundling the handling of a higher electionEpoch into a single guard. To catch this, Transition Validation splits actual execution traces into (pre_state, action, post_state) windows and validates them action by action.

The results showed the syntax stage came close to nearly 100%, but scores dropped sharply for conformance and invariant. In particular, performance was weak on complex distributed systems like Etcd, RedisRaft, CURP, PGo raftkvs, and some models' overall scores were as low as 25%.

The remaining challenges are clear.

• Trace coverage needs to be broadened further
• Information loss caused by state abstraction needs to be reduced
• Automation of harnesses, invariant templates, and validation modules for new systems is needed