SysMoBench shows why a compiling TLA+ model can still be wrong
An AI-generated formal specification can look reassuring: the module parses, the model checker runs, and the output resembles the protocol from a textbook or paper. It may still describe a different system from the code in front of you.
SysMoBench measures that gap. The open benchmark asks models to write TLA+ specifications for real concurrent and distributed systems. It then goes past syntax, comparing model transitions with traces from the code and checking expert-written invariants. For teams adding formal methods to a coding-agent workflow, a runnable specification is only the first checkpoint.
A Raft model is not necessarily an etcd model
The researchers explain the problem in an ACM SIGOPS article. They asked Claude to model etcd's Raft implementation. The generated TLA+ passed syntax checks and ran under TLC, but it mostly reproduced abstract Raft instead of etcd's implementation details.
A model can know the familiar shape of Raft without understanding how one codebase divides an operation, stores votes, or updates state. Correct formal syntax does not repair a wrong abstraction.
The current SysMoBench repository contains 11 systems. They include synchronization primitives from Asterinas OS, a ring buffer, etcd and Redis Raft, Xline CURP, ZooKeeper coordination, and PGo-compiled distributed systems. Each task pairs source code with an instrumentation harness and an invariant template.
The project's ICLR 2026 paper focuses on complete, realistic systems rather than small code fragments. TLA+ suits that job because it describes concurrent and distributed systems as states and transitions. The official TLA+ documentation explains that TLC checks finite models of TLA+ specifications for invariant violations.
Four checks produce different evidence
SysMoBench runs every generated specification through four phases:
- Syntax checking asks whether SANY can parse the module and decompose its actions.
- Runtime checking asks whether TLC can execute the model and reach its actions.
- Transition validation compares pre-state, action and post-state windows from real execution traces with transitions allowed by the specification.
- Invariant verification checks expert-defined safety and liveness properties against the generated model.
In the repository's canonical aggregate, syntax and runtime receive 15 percent each. Transition conformance and invariants receive 35 percent each. The weighting reflects the benchmark's purpose. Matching the system and preserving the properties engineers care about count for more than formatting a plausible model.
The authors report that most tested models cluster near 100 percent for syntax. Runtime scores range from 30 to 92 percent. The bigger failure appears later: leading models averaged about 46 percent on conformance and 41 percent on invariants. These numbers come from the authors' May 2026 reruns. Their live leaderboard can change as models and the benchmark change.
The wrong set can still type-check
ZooKeeper Fast Leader Election gives a clear example. In the implementation, each server stores received votes in a map keyed by sender. A new vote from the same peer replaces the old one. One generated specification used a set union instead, preserving both votes.
The pattern is reasonable in an abstract protocol and wrong for this code. Once quorum logic counts those entries, the specification reaches states the implementation never reaches.
The reverse also happens. A generated model combined a clock update and message handling into one guarded action. ZooKeeper performs them as separate steps. Treating them as atomic erased intermediate states that the real system enters during an election.
Both errors live in the relationship between model and code, not in TLA+ grammar. This resembles a coding agent producing a passing unit test that restates its own implementation. The artefact is internally consistent but does not check the external behaviour that matters.
Trace validation has limits
SysMoBench cuts captured executions into transition windows: (pre_state, action, post_state). TLC checks whether the named action can produce that change. A failure points to one action and one trace window instead of leaving reviewers with a single aggregate score.
The benchmark also states what this method cannot prove. A trace says nothing about a path it never exercises. State abstraction may discard information needed by actions that inspect detailed log contents. Adding another system still requires a hand-written harness, invariant template and transition-validation module.
A high conformance score therefore means the specification matched sampled transitions under the chosen abstraction. It does not prove equivalence across all possible executions. Formal verification still depends on the model boundary and on properties selected by people.
A review loop for AI-written specifications
Teams can use the same principle without reproducing the whole benchmark:
- Before generating TLA+, ask the agent to name the source files, state variables and implementation actions it plans to model.
- Run the parser and TLC, while treating both as basic validity checks.
- Capture executions that include retries, replacement updates, partial failures and reordered messages.
- Turn those executions into transition windows and check them against individual specification actions.
- Write important invariants independently. If one agent writes the implementation, model and oracle, the same misconception can survive all three.
- Review uncovered actions and lossy abstractions. A window count of zero means missing evidence, not a pass.
The repository exposes a command for one task, model and metric:
sysmobench --task spin --method direct_call --model claude --metric compilation_check
The complete suite needs more infrastructure, including Python, Java, Docker and build chains for some target systems. It also uses a coding-agent CLI during transition validation and invariant translation. That makes SysMoBench more suitable for research or platform evaluation than a lightweight continuous-integration job.
An evaluation service built with api.ish.chat can borrow the four-stage schema: store syntax, executability, trace conformance and invariant results separately. Do not flatten them into one pass flag. In ish.chat, a developer can use different models to critique the abstraction and draft adversarial traces before accepting the specification.
Our guide to coding-agent trajectory evaluation makes a related point. A final artefact hides how an agent reached it. SysMoBench adds another problem: even a clean artefact may describe familiar theory instead of the actual repository.
Compilation starts the review
AI can make a first formal model cheaper to produce, which may help teams that would otherwise write no specification. The benefit disappears when a familiar protocol template is mistaken for a faithful account of the code.
Keep the four results separate. Syntax says the module is well formed. TLC execution says the selected finite model can run. Trace conformance connects actions to observed code behaviour. Invariants test whether the abstraction preserves the properties that justified writing it.
Until an AI-written specification passes those last two reviews, its status should remain "draft," even when every line compiles.
