SysMoBench: Evaluating AI on Formally Specifying Complex Real-World Systems
Authors: Qian Cheng
Ruize Tang
Emilie Ma
Finn Hackett
Peiyang He
Yiming Su
Ivan Beschastnikh
Yu Huang
Xiaoxing Ma
Tianyin Xu
Venue: ICLR 2026 Poster (2026)
Keywords: Specification
Benchmark
Distributed System
Concurrent System
Agentic AI
Large Language Model
Primary area: datasets and benchmarks
TL;DR: A benchmark for evaluating AI's ability to formally model real-world systems.

Abstract: Formal models are essential to specifying large, complex computer systems and verifying their correctness, but are notoriously expensive to write and maintain. Recent advances in generative AI show promise in generating certain forms of specifications. However, existing work mostly targets small programs, not complete systems. It is unclear whether AI can deal with realistic system artifacts, as this requires abstracting their complex behavioral properties into formal models. We present SysMoBench, a benchmark that evaluates AI's ability to formally model large, complex systems. We focus on concurrent and distributed systems, which are keystones of today's critical infrastructure, encompassing operating systems and cloud infrastructure. We focus on TLA+, the de facto specification language for concurrent and distributed systems, though SysMoBench has been extended to other languages. We address the primary challenge of evaluating AI-generated models by automating metrics like syntactic and runtime correctness, conformance to system code, and invariant correctness. SysMoBench currently includes eleven diverse system artifacts: the Raft implementation of Etcd and Redis, ZooKeeper's leader election, the Spinlock, Mutex, and Ringbuffer in Asterinas OS, etc., with more being added. SysMoBench enables us to understand the capabilities and limitations of today's LLMs and agents, providing a firm footing for tools in this area and opening up promising new research directions.

Published as a conference paper at ICLR 2026
SYSMOBENCH: EVALUATING AI ON FORMALLY MODELING COMPLEX REAL-WORLD WORLD SYSTEMS
Qian Cheng Ruize Tang Emilie Ma Finn Hackett* Peiyang He
Yiming Su Ivan Beschastnikh Yu Huang Xiaoxing Ma Tianyin Xu
State Key Lab of Novel Software Technology, Nanjing University, China, {eq. peiyang he @esmal.njju.edu.cm {xxm, yuhuang) ) @nju.edu.cn Microsoft Research Asia, ruizetang @ microsofttcom
University of British Columbia, contact @ emilie. {fhackett, bestchai) @cs.ubc.ca University of Illinois Chaap--ham,,ign, (yiming34, tyxu) @illinois.edu
ABSTRACT
Formal models are essential to specifying large, complex computer systems and verifying their correctness, but are notoriously expensive to write and maintain. Recent advances in generative AI show promise in generating certain forms of specifications. However, existing work mostly targets small programs, not com- plete systems. It is unclear whether AI can deal with realistic system artifacts, as this requires abstracting their complex behavioral properties into formal models. We present SYSMOBENCII, benchmark that evaluates Al's ability to formally model large, complex systems. We focus on concurrent and distributed systems, which are keystones of today's critical infrastructure, encompassing operating sys- tems and cloud infrastructure. We focus on TLA*, the de facto specification lan- guage for concurrent and distributed systems, though SYSMoBENCH has been extended to other languages. We address the primary challenge of evaluating Al- generated models by automating metrics like syntactic and runtime correctness, conformance to system code, and invariant correctness. SYSMOBENCI currently includes eleven diverse system artifacts: the Raft implementation of Eted and Re- dis, ZooKeeper's leader election, the Spinlock, Mutex, and Ringbuffer in Asteri- nas OS, etc., with more being added. SYSMOBENCH enables us to understand the capabilities and limitations of today's is LLMS and agents, providing firm footing for tools in this area and opening up promising new research directions.
INTRODUCTION
Formal models are essential to specifying computer systems and reasoning about their correctness.
They provide mathematical foundation to verify the design of complex systems, such distributed
protocols and concurrent algorithms (Lamport 2002 Tasiran et al., 2003) Newcombe et al. 2015
used describe system implementations system code that runs on user devices and in production environments. Such system models enable
Hackett et al. 2023b). Recently, formal models
verification of system code via comprehensive testing and model checking (Bornholt et 2021
Tang et al. 2024 Ouyang et al., 22255] Tang et al. 2025). For example, system models of ZooKeeper
were used detect deep bugs that violate system safety and verify their fixes (Ouyang al. 2025)
However, system models are notoriously expensive to write and maintain. Different from protocols and algorithms, system code contains low-level details, is more complex, and constantly evolves. Hence, synthesis of system models is an open challenge (e.g.. TLAi+ Challenge (2025).
Recent advances in generative AI, represented by large language models (LLMs) and agentic tech- niques, show promise in generating function- level specifications, in the form of pre- and post- conditions (Rego al. 2025 Cao al. 2025 Xie et al. 2025 Chakraborty al. 2025 Ma al. 2025). This indicates that Al can capture certain behaviors of software programs. However, it is unclear whether Al could effectively model a complex system, which requires altogether different capabilities than the synthesis of pre- and post-conditions of a function. Modeling a system requires
"Corresponding author.

---

Published as a conference paper at ICLR 2026
System Artifact
Al (LLM Agents)
Quality Metrics
Fied Raft. Diertbuued kincaiiue ricre with conoreae strong conditanry
Generated Models
Syntac Correcinsis
Ue gloed ful mode and peraciionaae axcrme
100%
Rurtine Comectricaa
Code:
caliige
stompruge
necti.go
etod coh.3a
Doc::
i) laoker electioound
Ingureal cationudd
.... PERILE stol, raft
CONSTANTS Server, Value
Corfo marce System implemeniat Cocs actoro carlo witsustt
10%
tem,
Traces:
Rext Timesun // Flectiin V Heartheat
term 11 'Ann Server [+> 0]
Inverint Comeetness
Figure I: SYSMOBENCH sources its tasks from real-world systems (e.g., Eted Raft in the figure). automatically evaluates the system models in TLA+ generated by Al with different metrics.
the Al to understand the system design (e-g., the underlying protocols and algorithms), reason about safety and liveness under unexpected faults and external events, and abstract system behavior into an executable program. It is unclear to what extent AI has such capabilities.
In this paper, we present MYSEOBE,,H a benchmark to evaluate Al's ability to formally model complex systems. We target all forms of generative AI, including LLMs and agentic techniques. We focus on concurrent and distributed systems, which are especially difficult to model. They also underpin critical modern infrastructure, like operating systems and cloud computing. We focus on TLA* the de facto formal specification language for concurrent and distributed systems ($2). SYs- MOBENCH be easily extended support other specification languages such as Alloy (Jackson 2012). PAT (Sun et al.] 2009), P (Desal et al., 2013). and SPIN (Holzmann) 1997). We have added support for Alloy and PAT (see Appendix B).
The key challenge of SYSMOBENCI is to automatically evaluate Al-generated models-how can tell if system model is of high quality? We did not find any directly applicable metrics in use by existing work on TLA+ specification generation. For example, Cao et al. (2025) only checks if the generated TLA- can be run by the TLC model checker (Yu et al. 1999). D. But successfully running TLC is not an indicator of whether the model correctly describes the system. One approach to evaluate Al-generated pre-/post-condition (Rego al,, 2025; Ma et al. (024)) against human-
written reference specifications. However, such a comparison can be brittle, and real-world systems rarely have such low-level specifications. Writing a system model remains a highly challenging task that requires months to years of expert effort.
A key contribution of our benchmark is quality metrics that can be automatically checked. These metrics reflect the fundamental requirements of formal system model for use cases like formal verification (Lamport 2002) and model-driven testing (Clarke et al. 2018)).
Syntax correctness. We statically check whether the generated system model uses valid TLA+ syntax using the SANY Syntactic Analyzer.
Runtime correctness. We check how much of the generated TLA+ can be executed using the TLC model checker (Yu et al., 1999). which is a proxy for logical self-consistency.
Conformance. We measure whether the model conforms to the system implementation via trace validation (Cirstea et al.) 2024 Tang al. 2025 Hackett & Beschastnikh 2025).
Invariant correctness. We model-check the system model against system-specife invariants that reflect the system's safety and liveness properties.
SYSMOBENCH currently includes eleven real-world artifacts, including distributed systems like Eted, Redis, and ZooKeeper, and concurrent systems like spinlock, mutex, and ringbuffer from Asterinas OS. We also include system artifacts synthesized by PGo (Hackett et al. 2023a) to evaluate Al's ability to comprehend generated system code. More system artifacts are actively being added.
SYSMoBENCH enables us to understand the capabilities and limitations of AI in using TLA+ to model real-world systems by evaluating different agent designs with various AI models. State- of-the-art LLMs show good performance in modeling small system artifacts such as a spinlock implementation. On the other hand, these LLMs show limited ability comprehend and abstract large, complex systems such as a Raft implementation (Ongaro & Ousterhout 2014). Overall, we believe that SYSMOBENCH can spur innovative AI approaches in the context of formal system models, similar to the role of SWE-bench (Jimenez et al. 2024) in software engineering.
SYSMOBENCH can be found here: https://gtthbb.cc//p/pcllllloopp
2

---

Published as a conference paper at ICLR 2026
2 BACKGROUND
SYSMOBENCH focuses on formal models written in TLA [Lampor 2002), which is the de facto specification language for modeling distributed and concurrent systems in practice. TLA* is chosen from practical standpoint, not language standpoint (SYsMOBENCH supports other specification languages; Appendix B). TLA+ is widely used by software companies like Amazon, Microsoft, Nvidia, Google, Oracle, etc. (see TLA+ Foundation (2025)) verify critical infrastructure sys- tems such as distributed consensus systems (e.g.. Eted and ZooKeeper), confidential consortium frameworks (Howard al. 2025), databases (e.g.. CosmosDB and MongoDB), OS kernel synchro- nization (Tang et al. 2025). and cache coherence (Beers) 2008).
TLA+ model specifies system behaviors as collection of state variables, an initial predicate that defines their initial values, next-state relation that determines state transitions, and temporal properties that specify correctness requirements. The next-state relation is expressed as multiple actions, each describing an atomic state update of all variables. TLA is built upon the Temporal Logic of Actions (TLA), which includes and extends standard linear temporal logic (LTL) (Pnueli 1977,. providing rigorous mathematical foundation for reasoning about system behavior over time. TLA* models can be verified using explicit-stie state model checking via TLC Yu et al. 1999). sym- bolic model checking via Apalache (Konnov et al. 2019), and deductive verification Proof System (Chaudhuri et al. 2010). In SYSMo used TLA+ tool that systematically explores all reachable states of a system model to ensure that properties hold over the entire state space. These characteristics make TLA particularly well-suited for modeling complex concurrent and distributed systems.
the TLA we primarily use TLC, the most widely
pub struct SpinLock-T> lock: AtamicBool } pub struct SpinLockkuurddT,, R: SpinLock guard: R,
CONSTANTS Threads
VARTABLES lock_state,
Init
}
lock_state FALSE / pc [t Vin Threads |>> "idle"]
impl-T> SpinLock<T> { pub const fn new(val: T) Self { SpinLock { lock: AtomicBool: :en((alse)
StartLock(t) =
/ pc[t] "idle"
A pe' [pc EXCEPT [[t] = "trying.blocking"
A lock_state" lock_state
pub fn lock($self) >> SpinlockGuard--> { aalf-acquir__lock)) SpinLockkuard guard: self }
Acquire(t) =
10
10
A pc[t] Vin "ttrying.loccknng" "spinning")
11
11
A lock_state
12
12
THEN / lock_state' TRUE pe' [pc EXCEPT l[t] "lacked"] ELSE pe' [pc EXCEPT ([t] "spinning"]
13
acquire_ ( {
13
14
while Iself. tryl.ttry.aquiire_llo ()
14
15
lock_state' lock_state
16
fn try how.ee.coopreeccccnneeeeee .is_ok()
>> bool { true)
16
Unlock(t)
self.lock.
17 / pc[t] "locked"
18
18
A lock_state' FALSE
19
A pe' [pe EXCEPT [[t] "idle"]
20
fn release
lack(dsel)) release_lacc(tsett)) {
an guard drop
20
Mext = VE Vin Threads:
21
21 StartLack(t)
Acquire(t) V Unlack(t) YatualExclusion =
22
22
23
}
23 Cardinality((t
Threads pc[t] "lacked"))
Figure 2: Simplified code that implements a spinlock in Asterinas (left) and an Al-generated TLA+ model (right). This spinlock represents one of the simplest systems in SYSMOBENCII
Figure 2 shows simplified code that implements a spinlock in the Asterinas operating system (Peng al. 2025) and the corresponding TLA + model that describes the code. The TLA+ model
generated by the Al agent we evaluate in $ The model defines constants such as Threads (line 1) and system-state variables such as lock s state and pc (line 2). The initial state Init (line 3) assigns initial values to all variables. Three actions are defined (lines 5-19) StartLtkr,,c Acquire, and corresoddng to the code logic, where Acquire combines the logic of acquire_lock and try.acquire_lock. Each action is enabled by certain conditions, e.g., StartLock is enabled when thread's pc is "idle"; ; then assigns next-state values to all variables.
To model the spinlock implementation, the Al must first understand the behavior of each function. Next, it must decide how to represent the system. This involves introducing variables, such as auxiliary ones like pc, and defining atomic actions that preserve concurrency semantics. Finally, the Al must specify correctness properties. For example, mutual exclusion (line 22) requires that in every state, at most thread can be in the "locked" state.
3

---

Published as a conference paper at ICLR 2026
Note that SYSMOBENCH concerns formal models of system implementations, system specifica- tions in the TLA* and formal method literature. A system model enables verification of system code, but does not necessarily capture design requirements (Stoica al. 2024). SYSMoBENCH does not target other forms of specifications, such as formal proofs (Chen et al. 2025) or function- level pre- and post-conditions (Ma et al. 2025).
3 SYSMOBENCH
SYsMOBENCH is a benchmark that uses real-world distributed and concurrent system artifacts to evaluate AI's ability formally model systems. Table lists the systems that have been integrated in SYSMOBENCH; we are actively adding more system artifacts (3.
Table 1: System artifacts that have been integrated in the SYSMoBENCH; "TLA+ LoC" refers to the Al-generated TLA+ models presented our evaluation results (
System
Type
Desc.
Source Lang.
Source LoC
TLA* LoC
Asterinas Spinlock
Concurrent Concurrent
Synchronization
Rust
213
151
Asternas Mutex
Synchronization
Rust
186
219
Asternas Rwmutex
Concurrent
Synchronization
Rust
250
Asternaas Kingbulter
Concurrent
Data Structure
Rust
615
123
Flod Kaft
Distributed
Consensus (Raft)
Go
2,159
385
Redis Raft
Distributed
Consensus (Raft)
C
2,394
349
Xline CURP
Distributed
Replication (CURP)
Rust
4,064
100
ZooKeeper FLE
Distributed
Leader Election
Java
5,360
PGo dqueue
Distributed
Distributed Queue
Go
175
75
PGo locksve
Distributed
Lock Server
Go
281
93
PGo rattkvs
Distributed
Consensus (Raft)
Go
3,163
508
3.1 TASK FORMULATION
Each SYSMOBENCH task comprises generating a system model for given system artifact (Ta- ble D. SYSMOBENCH does not concern how the system model is generated. It can be generated by prompting LLMs directly, with few-shot learning, or with agentic techniques that invoke exter- nal tools (we evaluate both in $5). Since system artifacts in SYSMoBENCH are real-world system projects, one can feed various data sources to the LLMs/agents, such as source code, documents, and runtime traces. This task mirrors real-world modeling workflows of human engineers.
Each task specifies the granularities at which to model the target system's essential behavioral prop- erties and state transitions. The required level of granularity is defined based on target use cases; our current use case is model-checking based system verification, so we require the same level of detail in prior verification and bug finding work. The model must include core actions that interact with other components, while excluding implementation details unrelated to system behavior. We evaluate behavioral conformance rather than structural equivalence, allowing fine iineggriined modeling of core actions as long as they preserve semantic obligations needed for verification. Each task con- cretely lists core actions that must be modeled and actions that should be excluded. Take Spinlock as an example (Figure 2 the requirements are specified as follows:
Handatory actions that must modeled:
The nodel must specify lock() and unlock( actions.
Atomic compare exchange operation on the lock variable.
Spinning when the lock is contended.
Actions should excluded
model:
RAII guard implementaticn details.
Non-core details (e.g., debug foratting and trait implementation).
Besides, the task also requires generating a TLC configuration part of the model.
4

---

Published as a conference paper at ICLR 2026
3.2 METRICS AND THEIR MEASUREMENT
Key contributions of SYSMOBENCH are to (1) define fair metrics for the quality of Al-generated TLA models, and (2) design practical techniques to automate metric measurements. SYS- MOBENCH does not rely human evaluation, which is hard to scale, especially for complex systems. We do not consider a-M--a---jjudge approaches, as we find these unreliable and unin- terpretable.
SYSMOBENCH includes four metrics that evaluate a TLA* model on syntax (33.2.1, runtime cor- rectness ($3.2.2). conformance to system code (33.2.), and invariant correctness ($3.2.4). The metrics are not independent, e.g., a model with syntax errors cannot be evaluated for other metrics. An executable model is evaluated for both conformance and invariant correctness. We design partial scoring schemes for every metric and normalize results to percentage values, making them easy to interpret. Figure iillustrates the metrics and the evaluation workflow.
SYSMoBENCH
Syntax Curreciness
Runtime Correctness
Conformance to System Implemmnnattonn
Caakereed Sae
TLA" Model
Harmos
Xisel
Xade
Dl Chorle)
(MA
stat,
Correcteans pustiits
Man ki Minddennter
Ceeloroed Brver
Space
Timeout
Invariant Correctness
V. stumecc
Elaction
Coverod
Emee
Ioe arlae Templax
Concertiol
Mirkl
Hearlboal
Flactis Harbbet
bewred Iheectias Soatts
Mesic: 65- Soxro, 055 Soote
Marii:
Matric 11
Metrics and evaluation workflow of SYSMOBENCH The red dashed boxes denote inputs provided by the system artifact: instrumented system for code traces and required invariants.
Figure 3:
3.2.1 SYNTAX CORRECTNESS
SYSMOBENCH uses the TLA- SANY Syntactic Analyzer (Lamport 2002) to check the models' syntax against TLA* grammar rules, operator usage, module structure, etc. Note that SANY checks the entire specification. If the model passes the SANY checks, it earns a full score. However, many AI Al-generated models fail; we thus need fine-grained analysis for partial scoring.
SYSMOBENCH offers per-action analysis for partial scoring by checking how many generated ac- tions are erroncous (and failed SANY). It encapsulates each action in the model into per-action model by adding necessary dependencies (e.g., constant declarations, variable definitions, etc.). It then uses SANY check the syntax of per-action model (only syntax correction is concerned in this step: no equivalence check). A partial score S represents the percentage of correct actions n. among ns,, Here, n, is determined by running SANY on each per-action mod-
the total actions n,, i... ule and counting those that pass without syntax errors, while n, is obtained by counting all action definitions in the original model. Note that the per-action checks do not account for inter-action dependencies: model that passes all the per-action checks can still fail. We use a weighted scoring scheme that gives equal weights per-action correctness and inter-action correctness. A model that passes the overall SANY check earns 100%, while passing only all per-action checks earns 50%. Only system models with 100% syntax scores will be evaluated for other metrics, because models with syntax errors cannot be compiled or executed (which is required by other metrics).
3.2.2 RUNTIME CORRECTNESS
For a syntactically correct system model, SYSMOBENCH next evaluates the model can be exe- cuted correctly. To do SYSMOBENCI performs bounded model checking and simulation using TLC, and then observes covered actions and runtime errors (if any) by parsing TLC's coverage re- port and error output. This model checking and simulation explores the state space without any invariant checking (see (3.2.4) During this state space exploration, SYSMoBENCH records all covered actions and the actions with runtime errors.
5

---

Published as a conference paper at ICLR 2026
We define metric M, that represents the coverage of actions without runtime errors: M, fr where n, is the number of covered actions that did not report enrors during state exploration, and ne is the total number of actions in the model. Models with no runtime errors can then be executed to explore state space. Only such models are evaluated for conformance and invariant correctness.
ni
3.2.3 CONFORMANCE TO SYSTEM IMPLEMENTATION
S SYSMOBENCH evaluates an executable model's conformance to the system implementation using trace validation (Cirstea et al. 2024). Trace validation checks whether system execution traces correspond to paths in the model's 's state space. SYSMOBENCH supports diverse trace validation mechanisms (Tang et al. 2025
Cirstea et al., 2024 Hackett Beschastnikh) 2025).
Specifically, to collect execution traces, system code is instrumented with logging statements. The instrumentation granularity matches the granularity requirements of the task. If the Al Al-generated model is coarser than the trace logs, conformance checking may fail; otherwise, we use missing- event inference techniques (Tang et al. 2025) to account for uninstrumented actions.
The key challenge of automatic conformance checking of any Al-generated models is to correctly map the elements in the model to elements in the system execution log. This is because Al will often use names that differ from those in system code. We solve this problem by using coding LLM (e.g.. (oouee--))) to (1) extract constants, variables, and actions from the input model and (2) map them the corresponding elements specified in the task requirement ($3.1).
The use of LLMs to automatically map elements in the model and code may raise reliability con- cerns. In experience, state-of-the-art LLMs accomplish this mapping task reliably ($4). This is because (1) the mapping task is simple and well-defined; (2) the generated models are derived from the system artifacts and thus largely follow the system's 's naming conventions; and, (3) our trace validation technique (Tang et al. 2025) can tolerate a certain level of missing variables or ac- tions, though we have not found such cases so far. similar use of LLMs for mapping is adopted in Bench (025) (discussed in $6
During trace validation across all traces, SYSMOBENCH keeps track of code actions that are covered and those that trigger errors. Specifically, SYSMOBENCH feeds the trace to TLC along with the model and records whether TLC successfully validates the trace. validation fails, SYSMOBENCI identifies where the mismatch occurred by analyzing TLC's trace validation output. To measure conformance, we define Mc as the coverage of code actions without conformance errors: M, = nq. where ne is the number of code actions that were covered during validation with no errors, and n, is the total number of actions in the instrumented code. We use instrumented code actions instead of model actions because this provides a stable, implementation-gronn grounded granularity that is consistent across different Al -egeerrad models.
3.2.4 INVARIANT CORRECTNESS
SYSMoBENCH also evaluates whether Al-generated models always satisfy invariants that describe the expected safety and liveness properties of the system. In principle, if a system model fully conforms to code, violations of these invariants would indicate bugs in system code; in practice, few Al-generated models achieved fine-grained conformance. Nevertheless, Al-generated models have demonstrated practical utility by successfully reproducing known bugs from previous system versions (Appendix C.2 Table 2 lists the invariants for the spinlock code in Figure 2 These
invariants are part of the benchmark defined by the task ($3.3.
Table 2: Example spinlock invariants
Invariants
Description
Type
Mutual exclusion
At most one process can be in the critical section at any time The lock state accurately reflects critical section occupancy
Safety
Lock consistency
Safety
No deadlock
Not all threads can be stuck spinning simultaneously Every thread eventually releases the lock it acquires The system eventually reaches a state where all threads are idle
Safety
Guard lifecycle
Liveness
Eventual release
Liveness
SYsMoBENCH addresses a similar challenge as in $32.3 it needs to automatically map the actions, variables, and data structures in the system model to those expressed in the invariants. For this,

---

Published as a conference paper at ICLR 2026
the invariants in SYSMOBENCH templates that contain description of the property, formal definitions, and example TLA* invariants. We then use an LLM to translate these templates into model-specific invariants that can be checked against the system model. For example, the following template defines the mutual exclusion invariant in Table
"AutuulExclusioo"
patural_languaee "Only thread access shared resource time" fornal descriptos: "No nore than one thread in the critical section" Cardinality((t Vin [hreads:pe[t] "in
tla Humplle:uttualxxlus
S SYsMoBENCH prompts the LLM with both the invariant template and the system model and asks it concretize the template using the model. This mapping is highly structured: the output substitutes the template's s variables and constants with those in the model. For example, the mutual exclusion invariant, Cardinality(f (in Threads: status [t] "locked" <= 1, is a concretization of the template by replacing pe with status and inccs with locked. We evaluate the reliability of this LLM-assisted concretization in $4
The invariants used by TLC during model checking, and SYSMOBENCH observes whether each invariant is violated. Specifically, for each invariant, SYSMoBENCH creates a separate model with that invariant and runs TLC independently. This allows SYSMOBENCH to record whether each invariant violated. We define metric M, that represents the fraction of invariants passed, denoted M₁ n4 where n; is the number of invariants that hold across the explored state space, and n, is the total number of invariants defined for the model. Models with higher M; of higher quality. When combined with runtime and conformance coverage metrics, higher M, increases confidence in the correctness of the input specification.
ne
3.3 ADDING NEW SYSTEMS AND SPECIFICATION LANGUAGES TO SYSMOBENCII
SYSMOBENCH provides an extensible framework to add more real-world system artifacts. To add a new artifact to MYSNOBE one needs to (1) prepare the system artifact (e.g., source code and documents); (2) create new task that specifies the abstractions and components model ($3.)); (3) develop an invariant template (3.2.4) that specifies correctness properties (safety and liveness); and (4) provide a harness for trace validation by instrumenting system code. In our experience, the effort to add a new system artifact to SYSMoBENCH is manageable. For example, adding Eted Raft took one SYSMOBENCH author four days; an Xline CURP contributor with no experience of SYSMOBENCI added the system to SYSMOBENCI in four days. Most of the effort is spent on instrumenting the system to collect execution logs for trace validation in order to measure confor- mance. Unlike other benchmarks ($6). SYsMoBENCH does not require writing reference models; in fact, we hope that some of the Al-generated models can eventually be adopted by real-world system projects.
SYSMoBENCH is extensible to formal specification languages other than TLA+ We extended SYSMOBENCH support Alloy (Jackson, 2012) and PAT (Sun al. 2009), demonstrating its generality. Details of these extensions and preliminary evaluation are presented in Appendix [ The results show that while our framework extensible, TLA+ remains the practical choice and can benefit from Al-driven techniques (existing LLMs are less familiar with Alloy and PAT).
4 EVALUATION SETUP
To evaluate AI's system modeling abilities, three agents powered by LLMs.
Basic Modeling Agent. This agent reflects the LLM's raw modeling abilities. The agent prompts an LLM with the system source code and the task requirement ($3.1 (see Appendix G).
Code Translation Agent. This agent uses an LLM to translate system code into equivalent TLA+ The agent translates code statement by statement (from the source language to TLA+) and then organizes these statements' control flow into a TLA+ model. The agent reflects LLM- based code translation capabilities. We SSpecula (2025)
code translation agent.
Trace Learning Agent. This agent does not code input, but tries to learn the system model from system traces. It prompts LLMs with the traces to infer the system model (see Appendix(H] (H). This agent reflects the capability of automata learning (Biermann & Feldman 1972) with L.LMs.
7

---

Published as a conference paper at ICLR 2026
We follow HumanEval (Chen et al. 2021): we each agent five times and evaluate the best output model. The agents can enhance the model via feedback loops (max. three iterations) the generated model cannot pass compilation has runtime errors. No human intervention is allowed.
We use four different LLMs to power the three agents: Sonnee-Sonne-44 (202505144 14), GPT-5 (20250807), Gemini-2.5-Ph (20250617), and DeepSeek-RI (20250528). We the SANY Syn- tactic Analyzer, TLC model checker, and system code (for conformance checking) on server with dual AMD EPYC 7642 48-Core Processors and 256GB RAM running Ubuntu 22.04.
Robustness of LLM-assisted Components. SYSMOBENCH uses LLM-assisted techniques to map elements in an Al-generated TLA+ model those in the system logs ($3.2.3). and to concretize invariant templates ( ($3.2.4). We inspected the LLM- -La-sssited mapping and concretization, and found the results to be correct. We also conducted an experiment using the "gold model" for Eted Raft and Asterinas spinlock, which are known to be correct. We created 10 models (5 for each system) by changing the names of the variables and actions and tweaking the model's granularity. The gold models achieve perfect score on all metrics, empirically validating the quality of our metrics.
Training Data Contamination. One may concerned about the fairness of SYSMOBENCH be- cause it uses open-source projects where the system code likely already appears in LLM training data. In fact, having system code in LLM training data is intended. The design mirrors how human engineers write formal models: they first learn system code before writing formal models. Our goal to leverage LLMs to write effective TLA models for important, safety-critical software systems, which requires LLMs to have internalized knowledge of these systems. Note that this is different from coding benchmarks that we ask LLMs/agents to write existing code.
Second, few system artifacts in SYSMOBENCH have TLA system models in their open-source repositories. The TLA models of Asterinas Spinlock/Mutee/Rwwmuree are never released. Redis Raft and Xline CURP do not have any TLA+ models. Eted Raft and PGo systems do have TLA+ models in the repositories. However, those models are for protocols, not for system code.
5 RESULTS
We present evaluation results for the basic modeling agent and the code translation agent on Aster- inas Spinlock and Eted Raft (Table 3). Appendix 1.2 contains the complete results for all systems in SYsMOBENCH. We omit the results of the trace learning agent (which fails to pass runtime checks).
Table 3: Evaluation results of two Al agents on two representative system artifacts. / and X mark whether the model is evaluated in the next phase of measurements (see Figure B
(a) Asterinas Spinlock
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00% / 100.00% /
100.00%
100.00%
GPT-5
100.00% / 100.00% /
80.00%
100.00%
Basic Modeling
Gemini-2.5-PP
100.00% /
100.00% /
80.00%
85.71%
DeepSeek-RI
100.00% /
100.00% /
80.00%
100.00%
Claude-Sonnet-4
100.00% /
100.00% /
100.00%
100.00%
GPT-5
100.00% /
100.00% /
100.00%
85.71%
Code Translation
Gemini-2.5-PP
100.00% /
100.00% V
100.00%
100.00%
DeepSeck-RI
100.00% /
100.00% V
100.00%
100.00%
(b) Eted Raft
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00%
25.00% /
7.69%
69.23%
GPT-5
47.87% x
Basic Modeling
Gemini-2.5-PPr
50.00% x
DeepSeek-RI
50.00% x
Claude-Sonnets
100.00% /
66.67% /
15.38%
92.31 %
GPT-5
100.0092 /
20.00% X
Code Translation
Gemini-2.5-Pa
44.44% X
DeepSeek-RI
100.00%
0.00%
8

---

Published as a conference paper at ICLR 2026
50-
39.89
38,0%
Peneeiage (96
20-
Ponsmingg (S)
21.39
Peteeninge (S5)
60-
16.2%
15.35
20
13.09
10-
4.7%
8.35
Tokes Eroos
Syabbll Degeation
Qperuttc Brces
Intensution Eiros
Odee Syzrax
Coafis Enos
Stuctuue Coappiiso
Staee Eouuesttio Ensus
Startuee Cycatton
Safety
Lineesss
(a) Syntax Errors
(b) Runtime Errors
(c) Invariant Violations
Figure 4: LLM error attribution regarding the SYSMOBENCH metrics in the basic modeling agent. The conformance metric is omitted as it has single attribution.
Modeling Capability. We focus on the results of the basic modeling agent. The basic modeling agent generate high-quality TLA models for Spinlock, which is among the simplest artifacts SYSMOBENCII (Table [ showing certain levels modeling capability. However, for larger and more complex systems such as the distributed protocol implementations. the basic modeling agent performs poorly. For Eted Raft, only with -ouude-- the modeling agent reaches the conformance and invariant checking, and scores are low. Clearly, the complexity and size of Eted Raft exceed the modeling ability of the L.MMs and agents.
For Eted Raft, the basic modeling agents struggle with (1) code verbosity, (2) protocol complexity, and (3) abstraction. Eted Raft has much more code than Spinlock, with low-level utilities (e.g.. for debugging) and implementation-spetee
comments, which often cause agents lose focus on essential system logic. Moreover, the Raft protocol (Ongaro & Ousterhout 2014) has more complex logic than a spinlock
terms of ordering and intricate conditions of state transitions. Both (1) and (2) make Eted Raft significantly more challenging for LLMs to comprehend the system artifact. For (3), Eted Raft presents significant abstraction challenges: concepts like distributed logs require nested data structures, demanding LLMSs to precisely express them using TLA language constructs.
The basic modeling agents also perform poorly on PGo systems (Appendix I.2 indicating limited LLM ability to comprehend machine- machine-generatee generated systems. Code in PGo-generatee systems is mix of compiler-generated patterns and runtime library (Appendix D The generated code is repetitive, and, while it borrows some variable names from the source specification, intermediate variables have synthetic, non-significant names, which provide few semantic clues to an LLM (or human reader).
Analysis Agents. For complex systems like Eted Raft, the code translation agent outperforms the basic modeling agent. We believe this is due to powerful LLM translation abilities (Yang et al.) 2024b). This approach allows to leverage symbolie control-flon analysis for rigorous synthe- sis and prevent logic hallucinations by adhering to system code. We also saw that LLMs would sometimes imitate classic TLA + models from their training set, missing important system-specific content.
Analysis Invariants. L.MSs violate very different types of invariants-only 8.3% of safety prop- erties are violated while 41.9% of liveness properties were violated (Figure This indicates lim- ited LLM ability to reason temporally. To understand these violations, we conducted fine- ine-grained analysis categorizing them by root causes (Appendix [.I). We find that while faimess assumption violations (e.g., missing or incorrectly specified assumptions) are significant issue across systems, logical and structural errors tend to manifest earlier before fairness-relate issues emerge.
Analysis on LLMs. We observe that LLMs constantly introduce syntax errors (Figure 4b), espe- cially GPT-5, Gemini-2.5-Pro, and DeepSeek-RI 1. For example, DeepSeek-RI R1 often misuses math- ematical symbols (e-g., n, V) instead of ASCII TLA+ operators. Gemini-2.5-Pro and GPT-5 tend to mix up TLA+ syntax with other languages like Python. LLMs also provide incorrect opera- tor parameters and produce malformed indentation. In terms of runtime errors (Figure 4p), LLMs frequently generate inconsistent TLC configs, with missing constants mismatched declarations. Misunderstanding TLA* data structures is also common, e.g., comparing incompatible types.
Claude-Sonnet-4 outperforms other evaluated LLMs in most metrics across evaluated system arti- facts. Since only syntax-valid models can proceed to subsequent evaluation phases, Claude-Sonnee 4's ability generate syntactically correct TLA+ models provides an initial advantage. However,

---

Published as a conference paper at ICLR 2026
its strength extends beyond syntax correctness. SYSMOBENCH decomposes evaluation into four distinct metrics that separate syntactic correctness from system behavior reasoning. As shown in Appendix L.2 for models that pass syntax checks, Mlaude-Sonnet-4 generally still achieves higher scores on runtime, conformance, and invariant metrics compared to other L.LMs.
Qualitative Assessment. We conducted qualitative evaluation assess Al-generated system model quality and utility in terms of bug finding (Appendix C.. Comparing with human-written TLA + models, Al-generated TLA models differ in structure and completeness but they capture essential system behaviors. Despite these limitations, Al-generated models have successfully reproduced known bugs in five systems, demonstrating their practical utility for partial correctness checking.
RELATED WORK
SYSMOBENCH is the first framework that evaluates Al on formally modeling real-world systems.
Benchmarks for Formal Specifications. There several benchmarks for evaluating LLMs and
Al agents on generating function-level pre-/post-condiiions and loop invariants (Rego et al.) 2025
Xie et al., 2025 Cao et al., 20255 Chakraborty al. [025] Ma et al. [2025] Wen et al. [2024). These
typically use small programs, such as Verilast data structure specs (Rego et al., (0255 and Leet-
Code programs (Ma et al. 2025). There also exist benchmarks for proof generation for deductive
software verification Yang et al. (024a)) and for verified code generation (Thakur et al. 2025 Ye
ct al. 2025). None of these benchmarks target real-world systems as in SYSMOBENCH. They fun-
damentally evaluate Al's abilities of code comprehension and specification, not system modeling.
Similarly, PAT-Agent (Zuo et al. 2025) and AlIoy-APR (Alhanahnah et all] 2025) target small tasks like puzzles and repairing injected errors (see Appendix B.3). The arguably most related benchmark
is TLAi+Bench (2025) which evaluates Al-generated TLA specifications, primarily logic puzzles.
It evaluates Al's ability use the TLA+ + language, not system comprehension modeling. Hence, TLAiBench and related benchmarks like Cao et al. (2025) only measure the syntax and runtime correctness of the TLA specifications. Li et al. (2025) develop a benchmark for Hyperkernel sys- tem call inference; however, it does not consider distributed systems or concurrency and assumes a ground-truth specification. As AI for code matures, the next step is capturing Al's benefits for prac- tically verifying real-world systems. We developed SY MYNNCH with this motivation in mind.
Our evaluation aims establish baseline of simple agents to reflect the status quo of Al abilities. More advanced agents, like those with domain-specific techniques such as [Bhatia et al. (024)) Wang et al. 2025), can be developed to improve the quality of AI- generrattedd models.
General AI Benchmarks. S MYSNOBENCH differs from general AI reasoning benchmarks such as MMLU (Hendrycks et al.) (02I). ARC (Clark et al., 2018), and HELM (Liang et al. 2022]. These benchmarks evaluate generic reasoning, knowledge, and problem-solving capabilities across diverse domains, while SYSMoBENCH focuses on the specific task of formally modeling large, complex software systems as a foundation of formal system verification. SYSMoBENCH also differs from benchmarks targeting AI agent safety such as Agent-SafetyBench (Zhang et al. 2024). It currently targets traditional distributed and concurrent systems that are implemented in system code without neural components. The formal system modeling tasks evaluated by SYSMOBENCH are not covered by existing benchmarks such as EvalScope (EvalScope 2024).
CONCLUDING REMARKS
This paper presents MYSMOHEN,H, new benchmark for evaluating generative Al in formally mod- cling real-world systems. This goal pushed us to articulate criteria for formal system models and to develop automatable metrics. We find that despite strong coding and debugging abilities, modern AI remains limited in comprehending and specifying complex systems. We hope SYSMOBENCH will help advance AI technologies towards software system intelligence, rather than code intelligence.
We are actively adding new system artifacts and improving SYSMoBENCH's usability. We en- courage others to contribute their system artifacts. We are also exploring ways to measure the maintainability of Al-generated system models and considering ways include human evaluation.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGMENTS
We thank the TLAi* Challenge organized by the TLA+ community, which started this joint effort. Huang's s group is supported by the Frontier Technologies R&D Program of Jiangsu (BF2024059), the National Natural Science Foundation of China (62372222, 62025202), the CCF-Huawei Populus Grove Fund HUGG-eiiwwi2225555) and the Collaborative Innovation Center of Novel Software Technology and Industrialization. Beschastnikh's group is supported by the Natural Sciences and Engineering Research Council of Canada (NSERC), grant number RGPIN-2025-0668 Finn Hack- ett was partly funded by the MongoDB PhD) Fellowship Program.
ETHICS STATEMENT
We strictly obeyed the principles outlined in the ICLR Code of Ethics, and carefully examined potential ethical concerns, including potential impacts on human subjects, practices data set re- leases, potentially harmful insights, methodologies and upplications, potential conflicts of interest and sponsorship, disrrininatioobbasffaaneess concerns, privacy and security issues, legal compli- ance, and research integrity issues. We do not identify any potential risks. In fact, we believe that the work, together with its artifacts (c.g., the TLA models) will have positive impacts on the correctness of real-world computing systems and infrastructures.
REPRODUCIBILITY STATEMENT
We have made faithful efforts to ensure the reproducibility of our work. We have provided the details of work in the paper and its appendix, including the prompts, implementations, and complete results. We have open-sourced all the research artifacts described in this paper at sulhtpss:/// //gi thub. com/ com/sppcula-org/ SyyMMBeecchhhh sorccllaorrg//ysoeennhh
which documents how use and extend different parts of the benchmark. We expect that readers can easily reproduce our results reported in the paper. We also maintain an active forum to assist with reproduction problems and questions on how use and build on SYSMOBENCH.
REFERENCES
Mohannad Alhanahnah, Md Rashedul Hasan, Lisong Xu, and Hamid Bagheri. An empirical evalu- ation of pre-trained large language models for repairing declarative formal specifications. Empir- ical Software Engineering (ESE), 1--38, July 2025.
Robert Beers. Pre-rtl formal verification: an intel experience. Proceedings of the 45th Annual Design Automation Conference (DAC), June 2008.
Sahil Bhatia, Jie Qiu, Niranjan Hasabnis. Sanjit A Seshia, and Alvin Cheung. Verified Code Tran- spilation with LLMs. In Proceedings of the 38th Annual Conference on Neural Information Processing Systems (NeurIPS), September 2024.
A. W. Biermann and A. Feldman. On the Synthesis of Finite-State Machines from Samples of Their Behavior. IEEE Transactions on Computers (ToC), C-2166):59-5577, June 1972.
James Bornholt. Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. Using Lightweight Formal Methods Validate Key- Value Storage Node in Amazon S3. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles (SOSP), October 2021.
Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Chi Cheung, and Cong Tian. From Informal to Formal Incorporating and Evaluating LLMs on Natural Language Requirements Verifiable Formal Proofs. In Proceedings of the 63nd Annual Meeting of the Association for Computational Linguis- fies (ACI.), July 2025.
11

---

Published as a conference paper at ICLR 2026
Madhurima Chakraborty, Peter Pirkelbauer, and Qing Yi. FormalSpecCpp: A Dataset of C++ For- mal Specifications created using LLMs. In Proceedings of 2025 IEEE/ACM 22nd Interaational Conference Mining Software Repositories (MSR), April 2025.
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. The TLA+ Proof System: Building Heterogeneous Verification Platform. In Proceedings of the International Colloquium on Theoretical Aspects of Computing, September 2010.
Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fo- tios Chantzis, Elizabeth Barnes, Ariel Herbert- Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Josh Achiam, Vedant Mísra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Πya Sutskever, and Wojeiech Zaremba. Evaluating Large Language Models Trained on Code. arXiv:2107.03374 July 2021.
Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu K. Lahiri, Tao Xie, and Lidong Zhou, Automated Proof Generation for Rust Code via Self-Evolution. In Proceedings of the 13th International Conference Learning Representations (ICLR), April 2025.
Horatiu Cirstea, Markus A Kuppe, Benjamin Loillier, and Stephan Merz. Validating Traces of Distributed Programs against TLA+ Specifications. In Proceedings of the 2024 International Conference on Software Engineering and Formal Methods (SEFM), November 2024.
Peter Clark, Isaac Cowhey, Oren Etzioni, Tushar Khot, Ashish Sabharwal, Carissa Schoenick, and Oyvind Tafjord. Think you have solved question answering? try arc, the ai2 reasoning challenge. arXiv preprint arXiv:1803, 05457, March 2018
E.M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith. Model Checking. MIT Press, 2 edition, 2018
Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. P: Safe Asynchronous Event-Driven Programming. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PIDII), June 2013.
EvalScope. A framework for efficient large model evaluation and performance benchmarking. https://gi thub. http:///o//mmddeeeccceeeeesscp/p 2024.
A. Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do and Ivan Beschastnikh. Compiling Distributed System Models with PGo. In Proceedings of the 28th ACM International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS), March 2023a.
Finn Hackett and Ivan Beschastnikh. TraceLinking Implementations with Their Verified Designs. Proc. ACM Program. Lang., (OOPSLL), October 2025.
Finn Hackett, Joshua Rowe, and Markus Alexander Kuppe. Understanding Inconsistency in Azure Cosmos DB with TLA+. In Proceedings of the 45th International Conference on Software Engi- neering: Software Engineering in Practice (ICSE-SEIP), May 2023b.
Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. Measuring massive multitask language understanding. Proceedings of the Interna- tional Conference on Learning Representattonss (ICLR), May 2021.
Gerard J. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering (TSE), 23(5):279-295, May 1997.
12

---

Published as a conference paper at ICLR 2026
Heidi Howard, Markus A. Kuppe, Edward Ashton, Amaury Chamayou, and Natacha Crooks. Smart Casual Verification the Confidential Consortium Framework. In Proceedings of the 22nd USENIX Symposium Networked Systems Design and Implementation (NSDI), April 2025.
Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, February 2012.
Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R Narasimhan. SWE-bench: Can language models resolve real-world github issues? In Proceedings of the 12th International Conference on Learning Representations (ICLR), March 2024.
Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. TLA+ Model Checking Made Symbolic. Pro- ceedings of the ACM on Programming Languages, 3000SSL)):-30,, October 2019.
Leslie Lamport. Specifyiin Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Pearson Education, 2002.
Shangyu Li. Juyong Jiang, Tiancheng Zhao, and Jiasi Shen. OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification. arXiv:2504.20964, April 2025.
Percy Liang, Rishi Bommasani, Tony Lee, Dimitris Tsipras, Dilara Soylu. Michihiro Yasunaga, Yian Zhang, Deepak Narayanan, Yuhuai Wu, Ananya Kumar, et al. Holistic evaluation of language models. arXiv preprint arXiv:2211.00 1.00//10100000 10, November 2022.
Lezhi Ma, Shangqing Liu, Lei Bu, Shangru Li, Yida Wang, and Yang Liu. SpecEval: Evaluating Code Comprehension Large Language Models via Program Specifications. arXiv:2409. 12866, September 2024.
Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. SpecGen: Automated Generation of
Formal Program Specifications via Large Language Models. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE), September 2025.
Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Muntcanu, Mare Brooker, and Michael Deardeuff. How Amazon Web Services Uses Formal Methods. Communications of the ACM (CACM), 58 (4):66-73, 73, March 2015.
Diego Ongaro and John Ousterhout, In Search of an Understandable Consensus Algorithm. In Proceedings of the 2014 USENIX Annual Technical Conference (ATC), June 2014.
Lingzhi Ouyang, Xudong Sun, Ruize Tang, Yu Huang, Madhav Jivrajani, Xiaoxing Ma, and Tianyin Xu. Multi-Grained Specifications for Distributed System Model Checking and Verification. In Proceedings of the 20th European Conference Computer Systems (EuroSys), March 2025.
Yuke Peng, Hongliang Tian, Junyang Zhang, Ruihan Li, Chengjun Chen, Jianfeng Jiang, Jinyi Xian, Xiaolin Wang, Chenren Xu, Diyu Zhou, Yingwei Luo, Shoumeng Yan, and Yinqian Zhang. As- terinas: A Linux ABI-Compatible, Rust-Based Framekernel OS with Small and Sound TCB. In Proceedings of the 2025 USENIX Annual Technical Conference (ATC), July 2025.
Amir Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th Annual Symposium Foundations of Computer Science (FOCS), September 1977.
Marilyn Rego, Wen Fan, Xin Hu, Sanya Dod, Zhaorui Ni, Danning Xie. Jenna Di Vincenzzo and Lin Tan. Evaluating the Ability of GPT-4o to Generate Verifiable Specifications VariFast. In Proceedings of the 2nd IEEF/ACM International Conference on Al Foundation Models and Software Engineering (FORGE), April 2025.
Specula. A Framework for Synthesizing High-Quality TLA+ Specifications from Source Code. http::::/.iithbbb.mmmmppeuaaaaaa
2025.
Ion Stoica, Matei Zaharia, Joseph Gonzalez, Ken Goldberg, Koushik Sen, Hao Zhang, Anastasios Angelopoulos, Shishir G. Patil, Lingjiao Chen, Wei-Lin Chiang, and Jared Q Davis. Specifica- tions: The missing link to making the development of LLM systems an engineering discipline. 2.X0::2412.05299, December 2024.
13

---

Published as a conference paper at ICLR 2026
Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. PAT: Towards Flexible Verification Under Fair- ness. In International conference on computer aided verification (CAV), June 2009.
Ruize Tang, Xudong Sun, Yu Huang, Yuyang Wei, Lingzhi Ouyang, and Xiaoxing Ma. SandTable:: Scalable Distributed System Model Checking with Specification-Level State Exploration. In Pro- ceedings of the 19th European Conference on Computer Systems (EuroSys), April 2024.
Ruize Tang, Minghua Wang, Xudong Sun, Lin Huang, Yu Huang, and Xiaoxing Ma. Converos: Practical Model Checking for Verifying Rust OS Kernel Concurrency. In Proceedings of the 2025 USENIX Annual Technical Conference (ATC), July 2025.
Serdar Tasiran, Yuan Yu, and Brannon Batson. Using Formal Specification and Model Checker to Monitor and Direct Simulation. In Proceedings of the 40th Annual Design Automation Conference (DAC), June 2003.
Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue, and Swarat Chaudhuri. CLEVER: A Curated Benchmark for Formally Verified Code Generation. arXiv preprint arXiv:2505. 139388 May 2025.
TLA Foundation. Industrial Use of TLA+
http://foundaiion wwt.:aaiii....tlll.u.ino.oooooo.
index .tmll 2025.
TLAi+ Challenge. GenAl-accelerated TLA+ Challenge. rttp:://foumaatioonttap.... challenge// 2025.
TLAi+Bench. TLAi+ Benchmarks on TLA+ Formal Specification Tasks, https://github.com tlaplus 2025.
Bo Wang, Tianyu Li, Ruishi Li, Umang Mathur, and Prateek Saxena. Program Skeletons for Auto- mated Program Translation. Proc. ACM Program. Lang., 9(LDDI), June 2025.
Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Ching-Chi Cheung. and Cong Tian. Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. In International Conference Computer Aided Verification (CAV), July 2024.
Danning Xie, Byoung-Joo Yoo, Nan Jiang, Mijung Kim. Lin Tan, Xiangyu Zhang, and Judy S. Lee. How Effective are Large Language Models in Generating Software Specifications? In Proceedings of the 2025 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER), March 2025.
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. Vuruve Automated Proof Generation for Rust Code. arXiv:2409. 3082, September 2024a.
Zhen Yang, Fang Liu, Zhongxing Yu, Jacky Wai Keung, Jia Li, Shuo Liu, Yifan Hong, Xiaoxue Ma, Zhi Jin, and Ge Li. Exploring and Unleashing the Power of Large Language Models in Automated Code Translation. Proceedings of the ACM on Software Engineering, (FFS)) July 2024b.
7he Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song. VERINA: Benchmarking Verifiable Code Generation. arXiv preprint arXiv:2505.23135 May 2025.
Yuan Yu, Panagiotis Manolios, and Leslie Lamport. Model Checking TLA+ Specifications. Pro- ceedings the 10th IFIP WG 10.5 Advanced Research Working Conference Correct Hardware Design and Verification Methods, September 1999.
Zhexin Zhang, Shiyao Cui, Yida Lu, Jingzhuo Zhou, Junxiao Yang. Hongning Wang, and Minlie Huang. agent-safetybenchh Evaluating the safety of Ilm agents. arXiv preprint arXiv.2412.14470, December 2024.
Xinyue Zuo, Yifan Zhang, Hongshu Wang, Yufan Cai, Zhe Hou, Jing Sun, and Jin Song Dong. Pat-agent: Autoformalization for model checking. In Proceedings of the 40th IEEE/ACM Inter- national Conference Automated Software Engineering (ASE), November 2025.
14

---

Published as a conference paper at ICLR 2026
A ALTERNATIVE METRICS
No metric is perfect. Besides the core metrics presented in the paper, SYSMOBENCH also measures complementary metries that provide different measures of the system model quality.
A.1 RUNTIME PASS RATE
SYSMoBENCH repeatedly runs an agent to generate multiple TLA+ system models and evaluates whether each system model passes the runtime checks. The runtime pass rate is defined as Mar Raz, where Par is the number of TLA models that passed runtime checking, and not is the total nar'
number of generated TLA models. This metric complements the system model's action-level coverage metric M, (see $3.2.2), as reflects the agent's ability and reliability to produce fully executable TLA models. Note that high Mar does necessarily mean most actions in the TLA* models are correct. Even if some actions may contain runtime errors but are never executed during execution, the TLA model can still pass runtime checking. Conversely, a low Mar may result from a small number of frequently failing actions rather than errors affecting many actions.
A.2 CONFORMANCE PASS RATE
SYSMoBENCH repeatedly executes the system code to generate multiple code traces and checks which traces fully pass conformance checking. The conformance pass rate is defined as Mac nhr where Nae is the number of traces that passed conformance checking, and Nat is the total number of traces generated. This metric complements the code action-level coverage metric Mr (see $3.2.3) and provides coarse-grained empirical measure of the TLA+ model's overall alignment with ob- served system behavior. As with runtime correctness, low Moe does not necessarily indicate that most actions are unconformed, while high Mac generally suggests better overall system model quality, given sufficiently diverse traces.
B EXTENSIBILITY TO OTHER SPECIFICATION LANGUAGES
SYSMoBENCH is general specification languages beyond TLA+. To demonstrate its extensibil- ity, we extended SYsMoBENCH to support Alloy (Jackson 2012 and PAT (Sun et al., 2009).
B.1 SUPPORTING PAT AND ALLOY
PAT. PAT (Process Analysis Toolkit) a formal verification framework for concurrent and real-time systems. Supporting PAT in SYSMoBENCH is straightforward because PAT's tooling provides workflow similar to TLA+ We leverage PAT's parser for syntax checking, its simulator for runtime evaluation, and its assertion mechanism with model checking for invariant validation. Conformance evaluated using PAT's native trace refinement checker. We implement adaptors to translate our concrete system traces into the PAT format, which are then validated against the PAT models.
Alloy. Alloy is a declarative specification language based on first-order relational logic. For Alloy support, evaluating syntax, runtime, and invariant correctness is straightforward using the Alloy An- alyzer tool. Since Alloy does not provide a built-in notion of "action" " as in TLA+, we adapt the runtime metric by computing the proportion of variables and fields that become instantiated during bounded execution. This metric is analogous to the action-trigger coverage in TLA+ and it indicates whether model executes normally and whether certain branches are unreachable. For the confor- mance metric, we express a concrete system trace into Alloy facts, which are global constraints over a bounded sequence of states and must hold in all generated instances, for trace validation.
B.2 EVALUATION RESULTS
We evaluated the basic modeling agent with four LLMs (Claude-Sonnet-4, GPT-5, Semini-2.5-Pp and DeepSeek-BR R1) on generating Alloy and PAT models for the Spinlock system, with three attempts per LLM. Table 4 shows the results. For both PAT and Alloy, the four evaluation metrics (syntax, runtime, conformance, and invariant) remain applicable. However, due to limitations of current tools, syntax checking for PAT and Alloy does not support partial scoring in T
15

---

Published as a conference paper at ICLR 2026
Table Preliminary results of Alloy and PAT support on Asterinas Spinlock using the basic model- ing agent (3 attempts per LLM).
Language
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
0.00%
0.00%
0.00%
0.00%
GPT-5
100.00 100.00%
0.00%
0.00%
0,00%
Allay
Gemini-2.5-Pro
0.00%
0.00%
0.00%
0.00%
DeepSeek-RI
0.00%
0.00%
0.00%
0.00%
Claude-Sonnet-4
0.00%
0.00%
0.00%
0.00%
GPT-5
0.00%
0.00%
0.00%
0.00%
PAT
Gemini-2.5-Pro 0.00%
0.00%
0.00%
0.00%
DeepSeck-RI 0.00%
0.00%
0.00%
0.00%
The Al-generated Alloy and PAT models poor compared TLA+ models. For Alloy, only GPT- 5 was able to generate a model that passes the syntax correctness check after multiple attempts, but the generated model scored 0% on runtime correctness. For PAT, none of the evaluated LLMs demonstrated familiarity with the PAT syntax-all generated PAT models failed syntax checks.
Our analysis reveals that current LLMs are unfamiliar with the syntax of Alloy and PAT. In practice, nearly all generated models failed at the parsing type-checking stage. For PAT, LLMs frequently produced syntax borrowed from other languages such as C, Promela, PRISM. For example, chan- nels were often declared using PRISM-styl range expressions (e.g., channel acquire: ( ;) which PAT does not support. We also observed the introduction of keywords and type annotations that do not exist in PAT, such as adding explicit types (int) after variables using chan instead of PAT's actual channel declaration syntax. For Alloy, we observed similarly systematic breakdowns. A common pattern referencing signatures (types) that were never declared in the model, such as using Time module imports without defining what Time is. The models also wrote constraints that mixed incompatible language features, which Alloy does not accept.
We believe that the weak model capabilities using PAT and Alloy are primarily hecause Alloy and PAT are much less popular than TLA+ in real-world systems. Consequently, LLMs not exten- sively trained on these languages, resulting in poor generation quality. These results justify the use of TLA+ + the specification language of choice for SYSMOBENCIL
B.3 COMPARISON WITH RELATED WORK
PAT-Agent (uuo et al. 2025 and Alloy-APR (Alhanahnah et al. 2025 also evaluate Al's ability to work with formal models using PAT and Alloy, reporting promising results on their benchmarks. However, their tasks and complexity differ fundamentally from SYSMOBENCH. Table 5 summa- rizes the task of each work.
Table 5: Summary of the tasks of each work.
Work
Task
SYSMoBENCH
Generating formal models for real-workd software systems from their source code. Generating formal models from natural language descriptions.
PAT-Agent
Alloy-APR
Repairing an existing model with injected errors.
Because these tasks are inherently different, is difficult to compare their complexity directly. In- stead, we compare the complexity of the generated formal models shown in Table
Table 6: Complexity comparison across benchmarks measured by lines of code of formal models.
Benchmark
Smallest
Largest
Median
Task Type
SYSMOBENCH
75
508
219
Generation
PAT--gent
16
142
45
Generation
Alloy-APR (ARepair)
15
99
50
Repair
Alloy-APR (Alloy4Fun)
234
21
Repair
16

---

Published as a conference paper at ICLR 2026
Compared with the generation task in PAT-Agent most models expect LLMs/agents generate in SYSMoBENCH are larger than the largest models in the PAT-Agent paper. PAT-Agent's tasks small samples such river-crossing puzzles and restaurant workflows, not real-world software systems. Alloy-APR's tasks are similar, which come from ARepair and Alloy4Fun; neither of them uses weal- system artifacts.
To further validate our understanding, we reproduced the results of Alloy-APR and PAT-Agent using the same LLMs evaluated in SYSMOBENCI,, For Alloy-APR, used the official artifact on the ARepair benchmark. Table shows the results.
Table 7: Reproduction of Alloy-APR results on ARepair benchmark with LLMs used in SYS- MOBENCH.
Model
Correct Items
Success Rate
Claude-Sonnet-4
38 38
100.0%
GPT-5
30/ 38
78.9%
Gemini-2.55Prr
14 38
36.8%
DeepSeek-R1
5 3/
13.2%
Best result in Alloy-APR
28 / 38
73.7%
Our reproduction results show that Claude-Somnet-4 and GPT-5 outperform the best results reported in the Alloy-APR paper. This suggests that existing LLMS solve these repair tasks effectively- the high scores in the paper are largely due to the fact that the task itself is relatively simple. In contrast, results show that these LLMs still struggle generate syntax-correct Alloy models from complex system code in SYSNOBENCII (see Table 4).
For PAT-Agent, we ran the NoPlanning workflow using the LLMs evaluated in SYSMOBENCIL This workflow is similar to our Basic Modeling Agent: it calls the LLM to generate a PAT model and then iteratively fixes errors. Table g shows the results.
Table 8: Reproduction of PAT-Agent results using NoPlanning workflow with LLMs from SYS- MOBENCH. CSR: Compilation Success Rate, FPR: Full Pass Rate, APR: Average Pass Rate.
Model
CSR
FPR
APR
4
84.6%
80.8%
87.3%
GPT-5
84.6%
69.2%
76.4%
Gemini-2.5-Pro
84.6%
65.4%
74.8%
DeepScok-R1 57.7%
50.0%
54.9%
The results consistent with the original paper's findings. Similar to Alloy-APR, current LLMs can solve these relatively simple tasks to a reasonable extent (e.g.. Claude-Sonnet achieves 87.3% APR). However, their ability to generate formal models for real-world software systems is much weaker, as evidenced by our results (see Table
These results suggest that existing benchmarks such as PAT-Ageet and Alloy-APR mostly exercise simplified modeling tasks. contrast, MYSMO targets formal models derived from real sys- tem code, where current LLMs often fail to produce even syntax-correct specifications (see Table
C QUALITATIVE EVALUATION OF AI-GENERATED MODELS
Beyond the automated quantitative metrics, we performed qualitative evaluation to assess the prac- tical utility of Al-generated models for human engineers. We evaluated Al-generated models in two aspects: (1) comparison with numan-written ground- models from the community, and (2) their ability to reproduce known bugs in system code.
C.1 COMPARISON WITH HUMAN- WRITTEN MODELS
To assess the quality of Al Al-generated models, two human experts evaluated models produced by two different agents; the basic modeling agent and the code translation agent. Each expert compared AI- generated T models against human- muman-written models for nine of the systems in SYSMOBENCH.
17

---

Published as a conference paper at ICLR 2026
The experts identified ten main types of differences between AI Al-generated and human models (Ta- bles and
I0 summarize their occurrence across systems and LLMs):
1. Unnecessary EXTENDS/INSTANCE statements
2. Topics present in the human model but missing in Al models
3. Topics introduced by AI but absent in the human model
4. Fewer comments compared to human models
5. Properties present in human models but not in AI models
6. Different faireess assumptions compared to human models
7. Longer composite actions in Al models
8. Overly complex or random fairness conditions
9. Overspecialization with hard-coded values instead of parameters
Table Types differences between Al-generated models (produced by the basic modeling agent) and human- human-written models. Numbers refer to the types listed above.
System
Claude-Sonnet-4
GPT-5
Gemini-2.5-Pro
DeepSeek-RI
Asterinas Spin
1,3
1,5,8
1,
1, 8
Asterinas Mutex
1,5
1,5
1,5.9
Asterinas Rwmutex
1,5
1,5
1.5
Eted Raft
1, 5,7
1, 4,
1,2,4,5,7
1,2, 2,5,7
Redis Raft
1,4
1,4,7
1,4,7
1,4
Xline CURP
1,2, 4,5,
1, 5,
1,2,4,5,6
1,2,4,5,
PGo dqueue
1,5
1,5
1,5
1,5,7 1.5
PGo locksve
1,5
1.5
6,
PGo raftkvs
1.5.7
7.8
1,
1.5
Table 10: Types of differences between Al-generated models (produced by the code translation agent) and human-written models. Numbers refer to the types listed above.
System
Claude-Sonnet-4
GPT-5
Gemini-2.5-Pro
DeepSeek-R1
Asterinas Spin
2,
1,3,5, 6,
1,
1, 3, 5, 6, 1,2,
Asterinas Mutex
1, 1,2,5
1,2,
Asterinas Rwmutex
6,
1,3,
1,3,5,6
1,
Eted Raft
1, 6,
1,2,4.5,6
6,
1.
Redis Raft
1,3,4,5
1,3.4.5
1,3,4.
1,2,4,5,
Xline CURP
1,4.
4.5.
1,2,4.5,6
1,4,5,
PGo dqueue
5,
1,5,
1,5,
1,3,5,
PGo locksve
1,5
1,5,8
1,5
1,5,
PGo raftkvs
1,5,7
1,5,7,8
1,5,
1,5,6,7
We group and discuss these differences below.
Prompt-induced patterns (types 1, 4, 5). For both agents, many Al models include unnecessary EXTENDS INSTANCE statements (type 1), lack comments (type 4), and omit certain properties (type 5). These patterns largely result from our prompting and evaluation design. The prompt requires including common libraries to avoid syntax errors; this does not harm correctness or the evaluation of AI's modeling capability, human experts also sometimes copy-paste EXTENDS with unneces- sary dependencies. Missing comments and properties are expected, as SYSMoBENCH focuses on state/action modeling and does not require comment or property generation.
Model utility (types 2, 3, 6, 8, 9). Al-generated models may miss certain variables or actions (type 2) or include extra details (type 3), especially when there is significant difference in abstraction levels between the human-written models and Al-generated models. For instance, the code transla- tion agent tends to produce more concrete specifications compared to human- written ones, leading to more frequent occurrences of type (missing topics) and type 3 (extra topics). Faireess defini- tions (types 6 and 8) of Al-generated models often differ from human models or are overly technical random. which affect liveness checking. There also isolated cases of overspecialization (type 9). Overall, these differences show that AI models capture the general structure but may vary in completeness, fairness, and abstraction compared human models.
18

---

Published as a conference paper at ICLR 2026
Readability and documentation (types 4, 7). For both agents, the issue of fewer comments (type 4) is due to our prompt design; when we removed the instruction not to generate comments, AI models produced reasonably long comments that are easy to read. Some models also contain long composite actions (type 7) or use unconventional ordering of structure (e.g.. TypeOK checks placed unusually). Nevertheless, Al-generated models from both agents remain generally readable, with meaningful variable and action names and understandable structure.
C.2 BUG REPRODUCTION
Al-generated models can be practically useful for partial correctness checking. Without any hints about specific bugs, Al-generated models successfully reproduced several hard-to- fo-d bugs across multiple systems in SYSMOBENCI, Table I1 lists these reproduced bugs with links to the corre- sponding issue reports pull requests.
Table
Bugs successfully reproduced by Al-generated models.
Bug ID
Description
Eted Raft #10998
Learners cannot vote during promotion causing election failure
Xline CURP #402
Cluster will enter a frozen state after multiple crashes and recoveries
Redis Ralt #19
Stale reads under process pauses, violating linearizability
Asterinas Mutex #1279
Failed try clokk incorrectly unlocks mutex breaking mutual exclusion
Asterinas Rwmutex #1303
Lost wakeup when upgradeable reader releases lock
These bugs were discovered by having Al agents generate TLA* models from earlier versions of system code and then using model checking to identify the issues.
D EXAMPLES OF AI-GENERATED TLA MODELS
We present two Al-generated system models. Figures and 6 show the TLA+ model and its cor- responding TLC configuration for Asterinas Spinlock generated by the basic modeling agent with Claude-Sonnet-4. Figures 7 and show the TLA model and its corresponding TLC configuration for Eted Raft generated by the code translation agent with Claude-Sonnet-4.
MODULE spin
EXTENDS TLC, Sequences, SequencesExt, Naturals, FiniteSets, Bags
CONSTANTS Threads
VARTABLES
lock_state,
thread_states
guards
11
statc_sttte, thread_state,, guards>>
13
Type0K
15
lock state
Vin BOOLEAN
thread [Threads ("idle", "spinning", "locked"))
17
guards (subseteg Threads
19
Init
FALSE
21
thread_ state [t Vin Threads |>> "idle"]
guards ()
23
TryAcquire(t)
25
/N thread_state[t] Vin ("idle", "spinning")
FALSE
27
lock_state' TRUE
thread [thread EXCEPT [[t] "locked"]
29
guards' guards teup (t)
31 StartSpin(t) =
strted])stte(t]] "idle"
33
lock_state TRUE thread_state" [thread_state EXCEPT [[t] "spinning")
35
UNCHANGED staee, guards
19

---

Published as a conference paper at ICLR 2026
37
(pinLoop(t) =
(tread_state(t] "spinning"
39
lock TRUE
UNCHANGED selock_state, thread_state, guardsss
41
SpinAcquire(t)
43
/\ statelt] "spinning"
lock_state FALSE
45
lock_state, TRUE
thread_state" [thread_state EXCEPT [[t] "locked"]
47
guards' guards \eup (t)
49 TryLock(t)
(tread "idle"
51 A IF lock_state FALSE
THEN lock_state' TRUE
53
A thread_state' [thread_state EXCEPT [[t] "locked")
guards' guards (cup
55
ELSE A UNCHANGED sclock_state, thread_state, guardso>
56
57
Unlock(t)
threai_state[t] "locked"
59
\in guards
60
lock_state" FALSE
61
thread_state" [thread_state EXCEPT [[t] "idle"]
guards' guards
63
64
Next
65
TryAcquire(t) VE
Vin Threads:
66
67
StartSpin(t)
68
SpinLoop(t)
69
SpinAcquire(t)
Trylock(t)
71
Unlock(t)
73
Spec
Init / [[ext]]_Vaat Vars / M t Vin Threads: MF (Unloc((()))))
74
75
Figure 5: Asterinas Spinlock TLA model generated by the basic modeling agent with Claude-
Sonnet-4.
SPECIFICATION Spec
CONSTANTS
Threads (tl, t2, 13)
Figure 6: Asterinas Spinlock TLC configuration generated by the basic modeling agent with Claude- Sonnet-4.
MODULE etcdraft
EXTENDS TLC, Sequences, SequencesExt, Naturals, FiniteSets, Bags
Server,
1a Set of server IDs
Value,
1 Set of possible values for log entries
Mil,
Constant representing no value/no leader
Follower,
* Hode constants
PreCandidate,
datdidate,
11
Leader
13
VARTABLES
1. state[i] is the
15
currentlern,
1. current/orm[[] is the current ter of server i
votedFor,
18 votedFor[1]
voted for currentTem(1]
log, 17
1* log[i] is the log of server
InnditIndex, next Index,
18 Index(( is the comiit index of http://oweeerpttttoeeeeeeerrreee
19
* [3]]x is the next log index to send to server j from leader
natchIndex,
21
messages,
Set of nessages in transit
electionTimeout,
clectionTineoutt[1] tracks election tineout for leader(i] is the current leader known to server
23
leader
25 vars cestate, current votedPar, log, comitinnexx nextIndex, matchindex, messages,
electionTineout, leaders>
20

---

Published as a conference paper at ICLR 2026
27 1a Kessage types
MegHtu "Megitup"
29 MsgVote = "EsgVote"
MsgVoteResp "MsgWoteResp"
31 HsgPreWote = "nsoPreVote"
RegPreWoteResp
"MsgPreooteResp"
33 Megápp == "MsgApp"
MsgAppResp "nggAppRssp"
35 MsgHeaarteeat = "Ysgleeartbeat"
MegProp "MsgProp"
37
\ Helper functions
39 Min(a, b) IF THEN ELSE
Max(a, b)
THEN ELSE
41
LastTer(xxlog) IF Len(xlog) THEN ELSE xlog [Len(((o)))
43
Send(nn) nessages' nessages ccup
45
1A Initial
47
Init
28
state Vin Server |-> Follower]
49
currentierm [1 Vin Server |-> 0]
votedFor [i vin Server Nil]
51
log [i Vin Server 1-> cco]
comitIndex
Vin Server 1-> 0]
33
next [i Vin Server 1-> [j Vin Server |>> 1]]
54
matchIndex Vin Server 1>> [j Vin Server
55
nessages ()
56
electionTimeout
Vin Server |>>
57
leader [i \in Server 1-> Hil]
59 1a Election timeout triggers election
60 Timeout(i)
61
A stateli] Vin (Follower, PreCandidate, Candidate]
electionTimeout" [electionTinesut EICEPT [[]]
63
state" [state EXCEPT [[]] stateli] Follower THEN PreCandidate ELSE 0] IF state[i] Follawer
64
63
THEM Send[[type |-> MsgHlup from 1-> i, to 1>> i, tern |>> currentTerm(1])
66
ELSE messages' messages
67
A UNCHANGED <currentTern, votedFor, log, commitIndes, nextIndes, matchIndex, leader>>
68
69
\a Start prevote campaign
70 StartPreVote(l)
71
A state[i] PreCandidate
72
state' [state EXCEPT [1] PreCandidate]
73
LET lastIndex Len(log[i])
74
lastTern (lgg)))))oog(1))
75
messages' nessages \cup
76
[[type |-> MsgPreVote, from |>> i, |-> temm 1-> currentTerm[i] 1,
77
78
79
80
lastLogIndex lastIndex, lastLoggeem lastTerm]
81
Server (i))
82
UNCHANGED cocurennterr, votedFor, log, commitIndex, nextIndex, natchIndex, electionTineout,
Leader>>
83
84
1 Randle prevote response
85
Bandl SealleeePreoteeesponeec. It)
86
A n. type YsgPreVoteResp
87
n.
state[i] PreCandidate tern currentTern[1] +1
89
90
votes (msg Vin messages msg. type nsgetype
MsgPreVoteResp A
91
msg. to
92
msg. neg.term term currentTerm(i] + +1/ msg. voteGraattdd TRUE)
93
94
voteCount Cardinalityy from msg Vin votes)) \* self
95
IN IF voteCount Sardinality(Server) \div
96
THEN
state' [state EXCEPT [i]] Candidate]
97
currentTerm' TeurrentTern EXCEPT [ currentTem([]] 1]
98
votedFor' [wotedFor
[[i]
99
LET Index Len(log(i])
lastTerm LastTern(log(i)
IN messages' (nessages [m]) \eup
[[type XsgVote, from 1>> | j. term 1-> currentTern(i]
103
105
lastlogIndex LastIndex.
107
lastlogTerm |-> lastTerm] Vin Server (8)
21

---

Published as a conference paper at ICLR 2026
<<log connitIndex, nextIndex, matchIndex, electionTineout,
109
ELSE nessages nessages [M]
UNCHANGED currentTern, votedFor, log, commiiidex, nextindex, natchindex,
clectianTimeout, leaders>
112
1 Handle vote request
114
A n. type vin (XsgVote, HsgPreVote)
116
LET logOk = n. lastLogTer LastTem([oo (1])
/ m.lastLogTern LastTerm(log
118
A m.asttoogIndex >= Len(log (1])
grant
currentTemm(]
120
log0k
type MsgVote
122
THEN V votedFor = M1l
votedFor m.frrnn
124
ELSE TRUE
IN type
currentTerm1]
126
THEN A state" [state EXCEPT [[A] Follower]
[currentTern EXCEPT [ nerern]
128
votedFor' = [votedFor EXCEPT [[]] IF grant THEM n. from ELSE Ki1]
leader' [eader EXCEPT
Kil]]
130
ELSE IF n. type NsgVote A grant
THEN votedFor' [votedFor EXCEPT [[i] from]
132
A UNCHANGED eestate, current leaders> currentTers, votedFor, leaderss
ELSE UNCHANGED
134
A ([ype 1>> IF n.type NsgVate THEM KsgVoteResp ELSE MsgProVateResp,
from
136
to 1>> n.rrm, IF n.type NsgPreVote THEN ELSE currentTern' voteGrannted 1>> grant])
138
messages' messages (m) UNCHANGED <clog, indei,index, lnxe,, matchIndex, electionlimeouts>
140
142
\ HandTe vate response
Bandle WaneeeeWotRRssaseee
144 A n. n.type KsgVoteResp
146
state[i] Candidate
currentTern(i]
148
LET votes an (nsg Vin messages nsg. type MsgVoteResp A
msg.
150
msg. term term currentTern(i] A
voteGranted TRUE
152
voteCount Cardinality((nsg, from msg Vin votes)) 1" +1 for self vote
IN IF vateCount Cardinality(Server (div
154
THEM
state" [state EXCEPT [i] Leader]
leader' [leader EXCEPT [[i] =i]
156
nextIndex' [nextIndex EXCEPT [[i] Lf Vin Server 1>> len(log[i]) + 1]]
natchIndex' [matchIndex EICEPT [[i] [j Vin Server |-> 0]]
158
LET entry = Itern |>> currentTerm(i), value |-> Mil]
IN lag" [log EXCEPT [[i] Append(A, entry)]
160
messages" (messages (m]) \eup
[type |>> MsgApp.
162
from |->
to |-> 1->
164
term |-> currentTemm(j,
165
prevLogIndex 1>> Len(log(i)),
166
prevLogTerm 1-> lastTerm(Log(i))
entries |-> <centrys,
168
leaderCounit 1-> comitIndex(i]] Vin Server \ (i)}
UNCHANKGED <<currentTem,, votedFor, cindx, electionZimeout>>
ELSE
nessages' messages (m)
UNCHANGEE <<state, currentTern, votedFor, log, tIndx, nextIndex, natchIndex,
clectionTineout, leader>>
172
173
\ Client request (leader only)
174
ClientRequest(1, v)
175 A stateli] Leader
176
LET
[tern |>> currentTern(1,, value |-> v]
177
nexlog == Append(logli] entry)
178
IN
log' [log EICEPT [[1] newLog]
179
messages' messages \cup
[yype |>> XsgApp,
181
from |->
to >.
term currentTemm(1)
previogIndex 1-> Len(Log(i)),
prevLogTern 1-> LastTer((oog(1),
186
entries |-> <<entry>,
leaderCommit |>> comitinnex(ii]]
Server \ (i))
22

---

Published as a conference paper at ICLR 2026
scstate, currentTern, votedFor, nextIndex, matchIndex, electionTimeout,
leader>>
190
1 Bandle append entries
Chapenddeen n)
192
/ n. type MsgApp
194 IF u.terr currentTerm(1]
/A currentTem [currentTerm EICEPT [[i] m.temm]
196
A state' [state EXCEPT [1]] Follower]
votedFor' [votedFor EXCEPT [[i] Nil]
198
Leader' [leader EXCEPT [[A]
mrooon]
sccurrentTemm, votedFor>>
200
A IF n. tern currentTerm[1]
state' [state EXCEPT
202
ELSE UNCHANGED [leader EXCEPT [[A] = n.frrm]
leader' =
leaderss
204
mmectiontimeout lelectionTineout EXCEPT [4] 0]
LET log0k
prewlooggndex
206
A w.prevLogIndex <= Len(log [1])
log [n.prevooglndex] tem n.prevLogTerm
208
IN IF logok
THEN
log' [lg EXCEPT [[i] SubSeg(0, n.previ.ogineex) m.entries]
210
A commi LIndex' = [couni tIndex EXCEPT [i]] IF n. leaderroont conmitindex((]
THEN (en(m..eadderoomii Len(log [i]))
212
ELSE comitindex [i]]
(Lype | MsgAppResp, from | i,
214
from.
216
tern |>> currentTemn" [i],
TRUE,
218
matchindex 1-> m.. w..prevloogndex. Lem(n.entries)))
ELSE Send([type |+> MegApplessp
220
from |>> i, m.fron, tern 1>> currentiem [i],
222
FALSE,
224
matchindex 1-> 0])
URCHANGED <<log, connitIndex:>
226
nessages'
messages [m)
URCHANGED
<enextIndex, natchIndex
228
\ Randle append
250
Handl elopendResponseeL..... m)
nytyyee.. MsgAppResp A no
252
state[i] Leader
254
netern currentTern(i]
IF
236
THEN
/ matchIndex' [matchIndex EXCEPT [n.ron] n.macchIndex]
A nextIndex' [nextIndex EXCEPT [roon] m.natchIndex
258
A LET Agree(idx) [1] \cup {s Vin Server natchIndex' [i][s] >= idx)
agreeIndexes
(idx Vin 1. (enggl(())
240
Cardinallty(Servee)) Adiv / log[i] [1dx), term currentTern(1]
CeolinalityAAgreeeiie
242
comni tIndex' [comni tIndex EXCEPT [[]] IF agreeIndexes /= {)
THEN (3)) CHOOSE idx Vin
agreeIndexes
idx2 Vin agreeIndexes idx be
idx2)
ELSE commitIndex [i]]
246
ELSE A Inxe = Index EXCEPT [[]] fron] Max(1, next [3] [m. fron] 1)]
URCHANGED <enatchIndex, conmitIndex: messages [m] <estate, currentferm, votedFor, log, electionTineout, leaders>
248
messages'
URCHANGED
250
1 Send heartbeat
252
SendHeartbeat(()
mm state[i] Leader nessages' nessages lcup [[type Msgileartbeat, from i,
254
256
to term |>> currentTerm(i), leaderCommit |>> comitIndex(i]] Vin Server \ (1))
258
260
URCHANGED <estate, currentTern, votedFor, log, commitIndex, nextIndex, natchIndex, clectianTimenut, leaders>
261
\ Randle heartheat
263
Handl theartbett......... m)
nytype Ksglleartbeat
265
A n.
IF m.tern currentTern[i]
23

---

Published as a conference paper ICLR 2026
367
THEN ^
currentTerm' [currentTern EXCEPT [3] n.tem]]
state' [state EXCEPT [i] Follower]
269
votedFar' [votedFor EXCEPT [[4] Xil]
leader' [leader EXCEPT [[]] from]
271
A
diectionTimeout" [electionTimeout EXCEPT [[5] 8]
comi tIndex [comn tindex EXCEPT [[]] n.leaderCommit commitIndex
273
THEN Nin Min leadeerrrrmmt, (1]])
comni tindex
275
ELSE UNCHANGED escurrentTern, state, votedFor, leader, electionfimeout, commitindexos
nessages' messages (m)
277
UNCHANGED <clog, nextindex, matchIndexos
279
1 Advance election rimeout
AdvanceZlectiontiin
281
state[i] \in (Folloser, PreCandidate, Candidate]
electionTimeout [electionTineout EXCEPT [[i]
283
UNCHANGED costate, currentierm, votedFor, log, commitindex nextIndex, matchindex, messages, leader>>
284
Next
286
V
V i Vin Server Timeout(i)
Server StartPreVoteei)
258
V
VE i Vin Server, Vin messages Handl PaeedlePeeotteeeee erreloot m)
Server,
messages
eeteeeeeete... m)
290 V
VE i Vin Server, Vin messages
Handle Neteeeessss... (i, m)
Server.
Value ClientRequest v)
292 V VE i Vin Server, Vin messages Handl Appendantriesti n)
Server, SendHeartheat(1
messages canedddsppaditsssoncciiii
294 V VE Vin Server
Server,
messages elearbbbeatt
296
V AE i Vin Server AdvanceflectionTiine
298 Fairness =
(..vvar((inncott(t))
300
A VA i Vin Server WF vars
Server WF.var((VE Ván messages
RandllePreeeteReepnnseti m))
302
A VA i Vin Server WF vars(VE Vin messages
(andleloteRequestt., m))
Server WF.vars(VE Vin messages
BandleVooeResppnseei.. m))
304 A VA i Vin Server WV.vars(VE Vin messages
Hand HandleebpendEntriessG. n))
Server WF.vars(VE Vin messages
HandleeppennResponscci n))
306
A VA i Vin Server WE.vars(Senlkearbeat
varvars Vin nessages
Handlelfeartbeat((, n))
308
A VA i Vin Server
310
Spec Init / [] [Next] vars
A Fairness
312
Figure 7: Eted Raft TLA+ model generated by the code translation agent with Slaude-Sonner.e
SPECIFICATION Spec
CONSTANTS
Server (sl, s2, s3)
Value (v1,
Mil "Wil"
Follower "Follower"
PreCandidate "PreCandidate"
Candidate "Candidate"
10
Leader "Leader"
Figure 8: Eted Raft TLC configuration generated by the code translation agent with Claude-Sonnet-
E PGO-COMPILED SYSTEMS
Table T lists all the system artifacts in SYSMOBENCH. Unlike other open-source systems imple- mented mostly by human developers, PGo systems represent special kind of compiler-general systems. PGo is compiler converting distributed systems specifications written in a DSL of TLA into executable systems implementations in Go (Hackett et al. 2023a).
These systems reflect production use cases:

---

Published as a conference paper at ICLR 2026
dqueue is simple distributed queue with producers and consumers, which represents common cloud computing mechanism. Similar distributed queucs are available from many cloud platforms, like Amazon SQS, Cloudflare Queues, Apache Kafka.
locksve is simple distributed locking system, which represents common distributed systems concept.
raftkvs a verified distributed key-value store, with competitive performance. For its consensus implementation, raftkvs specifies Raft (Ongaro & Ousterhout 2014).
These systems are complex, each requiring several person-days of effort to specify. The raftkvs store is particularly complex, requiring almost person-month of effort. While they developed using a formal modeling language, these systems also account for practical coding concerns. Each system compiles usable, non-trivial Go code. Notably, raftkvs outperforms other formally verified key- value stores, with 41 % higher throughput than the next-best formally verified store implementation, and similar latency but 21% % of the throughput achieved by Eted.
A challenge unique to system modeling is that PGo-compiled systems contain machine- -eeiineegeeerteed Go code, which includes unusual abstractions and coding patterns. For instance, the generated code makes extensive use of abstractions from PGo's runtime support library, while containing many realistic engineering scenarios,
synthetically named variables. These issues are representative such generated code (macros, parser generators, state machines), or situations where the original source code lost (decompilation artifacts). This type source code input currently leads to poor performance on our benchmarks.
PGo Trace Validation. For Al-generated system models, we must validate their behavior against gathered execution traces. PGo's 's TraceLink feature provides a different trace validation method than for hand-written systems, allowing for automatic implementation tracing and TLA glue generation. As result, additional work is needed to gather traces. For simplicity, TraceLink's s published artifact. From these traces, TraceLink able to generate its own binding TLA+, mapping these logs precisely TLA+ + state space.
traces taken from
F SYSMOBENCH EVALUATION PROMPTS
During SYSMOBENCH evaluation, LLMs are invoked for conformance and invariant correctness evaluation to extract information, map actions and variables, and concretize invariants based on invariant templates.
We show the complete prompts used for benchmark evaluation. These prompts templates with parameterized fields that are instantiated by task-specific information. For demonstration, we in- stantiate the fields in the task for modeling Eted Raft, with the instantiated parts marked in green.
F.1 CONFORMANCE EVALUATION PROMPTS
Two prompts extract model information and map model action and variable names to code, both generating configuration files for script processing support trace validation.
Model component extraction. This prompt directs an LLM to extract TLA+ model components, such constants, variables, and actions, which used by script to generate trace specifica- tion (Cirstea et al.) 2024). A trace specification constrains state space exploration along the code trace path verify whether model state space path matches the code trace. In the prompt, the (oource_code] field is instantiated with the TLA+ model.
Model Component Extraction Prompt
Generate YAXL configuration file from the provided TLA- model (.tla) and configuration (.cfg) files. according to the following rules:
Extract in
## Task Description
Parse the TLA+ nodel configuration files create a structured YAMI configuration that captures model constants, variables, actions, and interactions.
Extraction Rules
25

---

Published as a conference paper at ICLR 2026
spec.name
Extract from the module declaration line: MODULE <NoduleName'>
The spec name is the ModuleNane between MODULE" and ".--=",
#*0 constants
Extract from the CONSTANTS section in the .cfy file.
identifier
value: The assigned value, formatted as:
Sets: Krap in single quates, e.g., "(si, s2, s3)" becomes "("s1", "s2", "s3")" single quotes double quotes inside, e.g., Nil becomes ""M11" Mrap single quotes string, e.g., becomes '5"
Strings:
Numbers:
variables
Extract from the Init operator definition in the .tla file.
For each variahle assigrment in Init:
nane: variable
default.value: The initial value expression (preserve TLA+ syntax, escape backslashes)
actions
Extract from the Next operator definition. Include only direct action calls (not numbered interactions). for each action:
action/eperator name parameters: List of paraneters with:
name: Parameter variable name
source:
paraneter comes (e-g., Server, messages)
The complete statement it appears in Rext (including any conditions)
interactions
Extract from the Next operator definition. Include only numbered internediate actions.
Just list the names (e.g., landletickklection.] Randletickieertteett..)
Example
Given this TLA+ model:
MODULE SimpleSper
A y [s Vin Server |-> 0]
Next
V VE s Vin Server Actionl(s) messages (ction2(n)
Internediatelction.
And this configuration:
CONSTANTS
Server (sl, s2}
MaxValue
Generate this YAML:
yaam
spec_name: SimpleSpec
constants:
name: Server
value: "("s1", "s2"}"
MaxValue
value: '10'
variables:
nane: deluult.value: '0'
name:
default.value: Win 1-> 0]'
actions:
name: Actionl
paraneters:
nane:
source: Server
ActionI(s)
name: Action2
paraneters:
source: messages
stat: Action2(m) (n)
26

---

Published as a conference paper at ICLR 2026
interactions:
name: Intermedlatekction.1
** Inportant Notes
Return ONLY the YAML content no explanations, comments, or natural language syntax exactly value fields (escape backslasbes) 3. For actions with conditions, include the full stnt it appears in Next
4. Ignore variables that appear Init but are not part of the main nodel (e.g., pc, info, stack) spec name, constants,
Order
actions, interactions
Generate the YAML configuration based on the provided TLA+ files:
(source.code)
Model and code component mapping, This prompt directs an LLM to map code to model vari- able naming for trace validation comparison. The LLM generates JSON file storing the mappings, which is further processed by script to output test harness that aligns code trace variable and ac- tion names with the model. In the prompt, the with the TLA model, and IMMPEMEENATION WWW.TTTOOCOOELLLACCLL.DDO with the corresponding code.
CEREC.COD_PLLCCHHOO PLACEHOLDER) field is instantiated
Model and Code Component Mapping Prompt
You tasked with generating JSON napping file that defines how convert concurrent distributed system traces to TLA+ model format for trace validation.
Systen Overview
distributed consensus algori thn impl empntttion that supports: Leader election with terns and prevoting/voting
Log replication across multiple nodes
State transitions between Follower, Candidate, and Leader roles
Message passing between nodes
Code Analysis
Before generating the napping, need analyze the relevant code to understand the system behavior:
your mapping on The examples for fornat reference only. Always the actual variables and actions defined in the provided model.
**RRTTICA**
model content, examples
*NP TLA+ Model Code "ttaa+ TTAASSPEC.OOE_PLACHHODDD
#** Implementation Code
go
## Input: System Trace Fornat
System
JSONL fornat with events like:
"json
:"coni": [["1", "2", "3"J, []), "log": 8, "name":
"InitState", "nid": "I", "role"s "StateFollover",
"state": ("comit": "tern":
"vote": "0"1)
("conf": [["1", "2", "3"], []]. "lag": 1, "name":
"BecomeCandidate"" "nid": "1% "rale":
"StateCandidate" "state": {"comnit"; 0, "tern":
1. "vate": "0"}}
("conf": [["1", "2", "3"], []], "log": "nane":
"BecomeCandidate" "hid": "2", "role":
"StatoCandidate". "state": ("comnit": 0, "tern":
1. "vate": "6"))
Common actions in systen traces:
BeconeFollower: Transition to follower role
deconeCandidate: Transition
BeconeLeader: Transition leader role
Ready: Mode is ready for operations
PreVote/Vote: Cast prevote/vote during election
AppendEntries: Replicate log entries
Heartbeat: Send/receive heartbeat nessages
## Target: TLA+ Model Variables
27

---

Published as a conference paper at ICLR 2026
The
variables: currentTerm: Current tern number for each node
state: Node role (Pallawer, Candidate, Leader)
votedFor: Which candi date this node voted for
commitIndex: Index of highest log entry know to be committed
nextIndex: For leaders, next log entry to send each server
matchIndex: leaders, highest log entry
replicated
Required Mapping Structure
Generate JSON file with this structure:
.. json
"config": {
"Server": ["Serverl", "Server2", "Server3"] List of identifiers
"events": {
systen actions "InitState": "Init",
events
"BecomeFol lover": "BecomeFollower' "BecomeCandidate:: "BecomeCandidate",
"Becomeleader": "Beconeleader", "Ready": "Ready",
"Vote": "Vate", "AppendEntries": "AppendEntriess,
"Heartbeat": "Beartbeat", mappings needed based code analysis
'node_napping":
Map string node IDs node names
"1": "Nodel".
"2": "Mode2",
"3"; "Node3",
Continue needed b.
"role_mapping":
// Map systen roles to TLA+ states
"StateFollower": "Follower",
"StateCandidate": "Candidate", "Stateleader"; "Leader"
Implementation Notes
The mapping will be used
tracker that maintains complete system
2. Server IDs in traces are numeric (0, 1, 2...) and must be napped to "Serveri", "Server2", etc.
3. The state tracker will automatically handle state transitions based actions
4. Forus correctly mapping actions and Server states
5. The config section should list all possible Server that night appear in traces
Your Task
Generate complete napping. file that:
1. Maps all commn actions their TLA+ equivalents
Provides ID nappings for
that appear
3.
Ensures compatibiltty with the state tracking implementatio
F.2 INVARIANT CORRECTNESS EVALUATION PROMPT
This prompt concretizes invariants from given invariant templates to model-specific forms. typically requires the LLM to map different names in an invariant template to the correspond- ing model elements. The $tla.model field is instantiated with the TLA model, and the $invariant templates field with the invariant templates defined in the system artifact (see $3.2.4 for an example).
Invariant Concretization Prompt
You are TLA+ expert specializing in distributed systems and Raft consensus, Your task is to implement expert-written invariants the given nodel.
Target Model
28

---

Published as a conference paper at ICLR 2026
Stla.nodel
** Invariants to enent
Sinvariant, Sinvariant.emplatees
Implementation Requirenents
1. *Deepp Analysis**; First, thoroughly understand both the invariant template's semantic intent and model's modeling approach:
What distributed consensus property does each template aim verify?
Now does the model represent server states, logs, terus, and leadership?
equivalents
template concepts model implenentation?
2. **Semantic happing**; For each invariant, identify the conceptual napping between template and model:
Template server concepts -> Model's server state representation
Template log structure +> Model's log data structures and indexing
Template leadership concepts -> Nodel's leader
management
Template node/server sets -> Model's 's server constants and domains
safety/livent neaning: *DDO NOT** simply replace variable names understand the underlying distributed systems logic **poRR redesign the predicate logic to fit the model's data structure gramulrrity
**Creative Adaptation**; Translate
preserving
**Do** equivalent senantic concepts if representations difffer
*"RESERVE** the original safety/Liveness guarantees without weakening the property
4.
Property Type Constraints*#;
**FOR SAFETY PROPERTIES** (type: "safety"):
**MUST** STATE PREDICATES (describe single states only)
**NEVER** prined variables ('currentTerm" 'lag"")
*"NEVIR"* use temporal operators (' '<>" '">"
**NEVER** reference actions (like 'RequestVote(s)" 'AApendEntries(s.t)) only use state variables
**ONLY** unprined variables ('currentTorm(s], 'log[s]' and constants
""CORRECT*"; 'LeaderUniqueness == \A term Vin Terms Cardinality((s Vin Servers state[s]
"leader" A currentTerm[s] term))
"IICORRECTT"" "state[s] "candidate" RequestVote(s)) (references action RequestVote)
(type: "liveness"):
**MUST** be TEMPORAL FORMULAS (describe execution traces)
**MUST** use temporal operators ('>>", ">>") ">") to express "eventually" or "leads-to"
**CORRECT**; Bventualleaderrieeetton <> (E Vin Servers state[s] "leader")
5. "CConstraint Compliance*";
Use ONLY variables, constants, and operators that exist in the model Generate complete, syntactically valid TLA+ invariant definitions
Kaintain the exact invariant names frem templates
6. **Output format**; Return ISON object containing array complete TLM+ invariant definitions
7. **EXTT naming requit;n You XUST use the exact invariant names specified in the templates
above.
Example Output Format
jjson
"Invariants":
cenderrUniqueness wu VM term Win MaxTerm
Cardinality((n Win Servers state[n]. role
\"leader\" /\\ state[n] currentTern tern)) <=
Win Servers Win DOMAIN log[ni] Win DOMAIN log[n2] A [og[n1]] ter. temm log [i]] term) => (VA Win 1..i [oo[n1][[]] [og[n2][i])"
"LogConsistency
}
"CRITICAA REQUIRENENTS**:
**SEMANTIC PRESERVATION** Each translated invariant MUST verify the same property as the original
template
simply onit invariants find creative ways express property using available model elenents
**CREATIVE ADAPTATION=*;
""COMPLETENESS* Ain to translate ALL invariants by understanding their semantic intent, not just their syntactic
Use ONLY variables, constants, and operators that exist in the provided model
Use EXACTLY the invariant nanes from the templates (preserve exact nanes for evaluation consistency)
29

---

Published as a conference paper at ICLR 2026
explanatory Each array element must be complete TLA+ invariant definition: "Invariantliane <expression
For camplex invariants, you may use mililiine format within the JSON string (use actual line breaks)
simple invariants, single line format preferred
**LAST RESORT"*; Only onit an invariant if its care concopt is fundamentally incompatible with the
model's design
*'CRITICAL J508 ESCAPING RULES
TLA+ operators like "\A", "VE", "kin' contain ONE backslash in the final TLA code
In 1508 strings, use EXACTLY ONE backslash escape: write "WW"" to get "M" in TLA-
.4D0 double-escape"n: ""WW""
will produce "WA" ILk+ *#CORRECT**; "LeaderUni queness == VM tem Win 1. MaxTer: state[tern] \"leader\ *"WOON"** "LeadertUniqueness: WWA tern Wiin 1..MaxTerm state[term] \"leader\
your response immediately
opening
G BASIC MODELING AGENT
The basic modeling agent operates in two steps for each system artifact: (1) generating the model, including both the TLA* + model and its TLC configuration, and (2) using feedback loop that takes SYSMoBENCH evaluation results to iteratively improve the generated TLA* model. We show the complete prompts of the basic modeling agent ($4) to provide detailed implementation.
MODEL GENERATION PROMPTS
TLA+ model generation. This prompt directs LLM to generate the TLA+ model file, in- stantiated with the granularity definitions the system artifact (see $3.1). .. The {file ppthh and soource_code, fields are instantiated with the code file path in the repository and source code content, respectively.
TLA Model Generation Prompt
You expert in formal veri fication and TLA+ models with deep expertise concurrent and distributed systems, particularly eted and Rašt consensus
Convert the following source code to comprehensive TLA- model.
System: eted distributed key-value
Source Code from (file path): go (source_code)
Systen-specific model ing requirenents:
HANDATORY ACTIONS include all):
1. [Message Types] MsgHup (election timeout), KsgVote/NsgWVoteResp (voting), Miggggg/MsgAppResp (log
replication
[Rode States] enabled)
StateFollower, StateCandidate, StateLeader, StatePreCandidate (prevote
3. [Leader Election] Complete prevote + vote phases: PreCandidate + Candidate + Leader transitions
[Log Operations] Log entry appending, consistency checks,
majority quorum
5. [HeartbeatTinnout] Election timeouts triggering campaigns, heartbeat prevention of elections [Client Proposals] MsgProp message handling and log entry creation by leaders
6.
EXPLICITLY EXCLUDED (do not model):
Configuration changes and joint consensus (ConfChange nessages)
Log compaction snapshots (XsgSnap)
ReadIndex optinizations (#sgReadIndex))
Asyne storage operations (Local4peendThread, Local4pplyThread)
flom control progress tracking details
REQUIRED BEHAVIORAL SCOPE:
phase (StatePreCandidate) must nodeled
enabled by default
State transition constraints: Follower + PreCandidate Candidate + Leader (strict transitions)
Xessage processing by state: only valid nessage types handled in each node state
Term advancement rules:
when receiving messages vote per tems, must be current or newer
higher
Voting restrictions:
Heartheat nechanism: leaders send heartbeats, followers reset election timeout on receipt
Log consistency peevoegIndee/prreeoogeee validation Nsgåpp processing
30

---

Published as a conference paper at ICLR 2026
Xajority-based
and log
Basic network nessage delays and losses
Generate model that accurately nodels the system's bebavior.
CRITICAL OUTPUT REQUIREMENTS:
MODULE (---- MODULE etcdraft -..-)
exactly "etcdraft
narkdown blocks " 3. Do not include explanations coments, or formatting narkers
pure
4. Start your response directly with: MODULE etedraft
5. End your response with the closing
6. =*00 NOT define invariants* (like KatualExclusion, Invariant, etc.) facus on nodeling the system
behavior
7. *XUST include EXTENDS statement**; The nodel must extend at least these modules: SequencesExt, Naturals, PiniteSets, Bags
TLC. Sequences,
TLC configuration generation. This prompt directs an LLM to generate TLC configuration file. The configuration file requires the LLM's understanding of the system to make the model executable, such as designating the initial predicate and next-state relations. The $tla_spec field instantiated with the TLA model generated in the previous step.
TLC Configuration Generation Prompt
You are TLA+ expert. Generate complete TLC configuration file (.cfg) for the eted model that can be directly saved and used for model checking.
#* Input Kodel:
Stla.spec
## Requirements:
"AAnalyee the =odel** to identify the main model name and all declared constants
2. **Generate complete .cfg file content*s with SPECIFICATION, CONSTANTS sections
small values constants**
efficient model checking servers, small integers)
4. **Output ONLY the raw .cfg file content** no explanations, narkdown, code blocks
Example Output
SPECIPICATION SpecName
CONSTANTS
**CRITICAL: Your response must contain exactly ONE complete .cfg file. repeat sections. Start your response imediately with "SPECIPICATION" and include nothing else.
G.2 MODEL REFINEMENT PROMPT
This prompt provides guidance for the LLM to refine the previously generated model using syn- tax and runtime evaluation results from SYSMOBENCH. The (current model} field contains the previous iteration's model, (current tlc cfg} contains the previous TLC configuration, (syntax (erorrr)errrr) contains the syntax errors reported by SANY, and (runtime.em sruntsme_errors] contains the runtime errors reported by TLC.
Model Refinement Prompt
You are an expert TLA+ model specialist with extensive experience in concurrent and distributed systems modeling.
I need you to fix errors in a TLA+ model for etcdraft systen.
#* Current TLA+ Model "tla
(current nodel)
Current TLC Con confiigration
31

---

Published as a conference paper ICLR 2026
fcurrent tlc.cfg)
Errors Found
**Detailed Syntax Errors:** (syntax_errors)
**Detailed Runtime Errors:*s )
** Correction Instructions
This is correction attempt (attenpt of (nax attempts).
Please provide corrected ILA+ model that fixes these errors. Your corrected model should:
**Fix syntax errors*h:
proper syntax, correct operator usage, valid
structure
2. **Resolve runtine errors*;; Define missing variables, operators, and ensure logical consistency original intent**: Keep distributed system logic behavior
source
code
4. *FFollww TLA+ best practices**; Use appropriate data structures, actions, and invariants
<aBe complete self-containeet:: Include all necessary EXTENDS, CONSTANTS, VARIABLES, operator definitions
Focus specifically on:
Defining any nissing variables constants Implementing missing operators functions
Fixing syntax issues
operators, expressions, module
Ensuring proper action definitions and state transitions
Maintaining consistency with etcdraft's system behavior
*CRITICAL OUTPUT REQUIRENENTS:""
Return ONLY pure TLA+ model code
code
(ne "'tla
"")
N0 explanations, comments,
outside the model
NO formatting markers of any kind
NODULE name must exactly "etcdraft"
Start directly with: MODULE etedraft
H TRACE LEARNING AGENT
The trace learning agent does not use any code as input; instead, it relies on the distributed traces as context. Similar to the basic modeling agent, we provide an initial prompt analogous to basic modeling agent's prompt ($G.T), but substituting the codebase context with trace information instead. the first model generation fails to pass compilation, the model refinement loop will pass the errors back to the LLM to iteratively fix the model.
Trace formats. The trace-based method works with several types of traces and can be easily ex- tended to additional systems. For each trace format, provide short custom prompt explaining the format. We currently support:
nnjsson and jsonn logs: Newline-delimited JSON, with coarse-grained logs defined by the specific system. One log file contains multiple nodes' execution logs.
PGo-instrumented logs generated by TraceLink (Hackett Beschastnikh, 2025
Also newline-
delimited ISON and contains PGo-specific concepts like archetype names and vector clocks. Vari- able updates are logged in fine- fine-grained detail each PGo-defined critical section. One log file is output per node; there are multiple log files per distributed execution.
Optimizations. We anecdotally noticed that passing single execution traces results in overfitting by the model, with generated models closely reflecting the single executed path. Providing more traces improves context for the model.
One issue we encountered was fitting large traces into models' context windows. The JSON structure of traces expensive in tokens, because each "[", ":", and other punctuation represents separate token. Most of the models we used had a context window of about 200K tokens; JSON trace of several megabytes, such the Eted Raft traces, simply could fit. We solved this with three workarounds:
32

---

Published as a conference paper at ICLR 2026
We support sampling for systems with large traces, randomly choosing of execution traces
among all collected traces.
We convert the nested JSON structure into tab-separated values (TSV) format, which deduplicates
JSON keys into the TSV header and uses only tabs separator save tokens.
We abbreviate repeated state action values (e.g.. ReceivvelerusstVoteeesppsss to acronyms (e.g., RRVR) and provide a mapping in the prompt.
The TSV and abbreviation optimizations significantly save tokens: with the Claude tokenizer, it reduces token use by 62% for ten lines of Eted Raft traces (from 645 262 tokens), and by 63% for ten lines of mutex traces (from 866 to 318 tokens). This enabled us to fit multiple traces into the initial prompt, reducing the impact overfitting We did not apply this optimization to the other methods, since code is less structured and does not have obvious candidates for deduplication.
I COMPLETE EVALUATION RESULTS
1.1 LIVENESS VIOLATION ANALYSIS
We analyzed counterexamples from two representative systems (Asterinas SpinLock and Eted Raft) and categorized liveness violations into two main classes:
Fairmess-relatee issues that prevent progress due to missing faimess declarations, overly narrow or overly broad constraints (e.g., defined as WF(Next));
Logical/structurall issues that block progress due to conflicting updates missing/incorrect logic in action definitions.
Since the modeling task focuses on state/action models of the system implementation and LLMs are required to generate temporal operators (e.g., in liveness properties), our categorization does not include errors related to temporal operators.
Table 12 presents the detailed breakdown of violations by category and LLM. For Asterinas Spin- Lock, Fairness-related issues dominate the violations, particularly "too broad" and "too narrow" constraints. For instance, -onudd--,nntt,,, generated 26 out of violations due to overly broad fairness assumptions.
For Eted Raft, liveness violations are primarily caused by logical/structual issues. The model's large state space causes these logical errors to block progress before carmess-related issues manifest. Nevertheless, manual inspection confirms that faimess conditions are generally incorrect.
Table 12: Liveness violations by category in Asterinas SpinLock and Eted Raft for the basic model- ing agent.
Asterinas SpinLock liveness violations by category
LLM
Fairness too broad
Fairness too narrow
Missing fairness
Logical errors
Total violations
Sluude-Sonnc--
26
2
32
GPT-5
8
10
20
Gemini-2.5-Pro
4
6
0
0
10
DeepSeek-RI
4
2
8
(b) Eted Raft liveness violations by category
LLM
Logical missing/errors
Conflicting updates
Total violations
Claude-Sonnet-4
4
12
GPT-5
2
20
Gemini-2.5-PP
DeepSeek R1
4
8
33

---

Published as a conference paper at ICLR 2026
1.2 DETAILED RESULTS BY SYSTEM
We present the complete evaluation results for all systems in our benchmark using three Al agents: Basic Modeling, Code Translation, and Trace Learning in Tables [3-23
These tables follow the
same evaluation setup as described in 4
Table 13: Asterinas Spinlock
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnct-4
100.00% /
100.00% /
100.00%
100.00%
GPT-5
100.00% /
100.00% /
80.00%
100.00%
Basic Modeling
Gemini-2.5-Prro
100.00% /
100.00% /
80.00%
85.71 %
DeepSeek-RI
100.00% / 100.00% /
80.00%
100.00%
Claude-Sonnct-4
100.00% /
100.00% /
100.00%
100.00%
GPT-5
100.00% /
100.00% /
100.00%
85.71% %%
Code Translation
Gemini-2.5-Pra
100.00% /
100.00% V
100.00%
100.00%
DeepSeek-R1
100.00%
100.00% /
100.00%
100.00%
Claude-Sonnet-4
50.00%
GPT-5
100.00% /
0.00%
Trace Learning
Gemini-2.5-Pro
100.00% /
0.00% X
DeepSeek- R1
100.00% /
0.00% X
The trace learning agent underperforms compared to the other two agents, typically failing compilation and runtime checks. We observe that it is more difficult for LLMs process structured trace data, in comparison source code. Specifically, Claude-Sone Sonnet-4 appears be particularly weak in this regard, achieving the lowest syntax scores, despite its coding capabilities. This trend of the trace learning agent is consistent across all the evaluated system artifacts (Tables 14 23
Table 14: Eted Raft
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00%
25.00% /
7.69%
69.23%
GPT-5
47.87% x
Basic Modeling
Gemini-2.5-Pro
50.00% x
DeepSeck-R1
50.00% x
4laude-Sonnet-4
100.00%
66.67%
15.38%
92.31 %
GPT-5
100.00% /
20.00% X
Code Translation
Gemini-2.55Pro
44.44% X
DeepSeek-RI
100.00%
0.00%
Blaude-Sonnet-
50.00% x
GPT-5
48.78% X
Trace Learning
Gemini-2.5-Pro
42.31 X
DeepSeck-RI
47.73% X
Table 15: Asterinas Mutex
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00% / 100.00% /
100.00%
100.00%
GPT-5
100.00% / 100.00% /
100.00%
85.71%
Basic Modeling
Gemini-2.5-PP Pro
100.00% /
100.00% /
66.67%
85.71%
DeepSeck-Ri R1
100.00% /
100.00% /
66.67%
100.00%
Claude-Sonnet-4
100.00% /
100.00% /
100.00%
100.00%
GPT-5
100.00% /
100.00% /
100.00%
100.00%
Code Translation
Gemini-2.5-PP
100.00% /
100.00% /
100.00%
85.71%
DeepSeek-RR R11
100.00%
100.00% /
100.00%
85.71%
Claude-Sonnet-4
50.00% X
GPT-5
50.00%
Trace Learning
Gemini-2.5-PP
100.00% /
0.00% X
DeepScck-Ri
50.00% X
0.00% X
34

---

Published as a conference paper at ICLR 2026
Table 16: Asterinas Rwmutex
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00% /
100.00% /
100.00%
90.00%
GPT-5
100.00% /
100.00% /
75.00%
80.00%
Basic Modeling
Gemini-2.5-Pra
100.00% /
100.00% /
0.00%
80.00%
DeepSeck-Ri R1
100.00% /
100.00% v
50.00%
90.00%
Claude-Sonnet-4
100.00% /
100.00% /
100.00%
90.00%
GPT-5
100.00% /
100.00% /
100.00%
90.00%
Code Translation
Gemini-2.5-PP P.o-Pro
100.00% /
100.00% /
100.00%
80.00%
DeepSeek-Re
100.00%
100.00% /
50.00%
90.00%
Claude-Sonnct-4
50.00%
GPT-5
100.00%
0.00%
Trace Learning
Gemini-2.5-Par
100.00% /
0.00% X
DeepSeck-RR R1
50.00% X
Table Asterinas Ringbuffer
Agent
LLM
Syntax
Runtime
Conformance
Invariant
4
100.00% /
100.00% /
100.00%
100.00%
GPT-5
100.00% /
0.00% X
Basic Modeling
Gemini-2.5-Pro
100.00% /
0.00% x
DeepSeck-RI
100.00% /
0.00% X
Claude-Sonnet-4
00000% /
100.00% /
100.00%
100.00%
GPT-5
100.00% /
100.00% /
100.00%
75.00%
Code Translation
Gemini-2.5-PP
100.00%
100.00% /
100.00%
100.00%
DeepSeck-RR R.
100.00% /
0.00%
Claude-Sonnet-4
100.00%
0.00%
GPT-5
100.00% /
0.00%
Trace Learning
Gemini-2.5-N
100.00% /
0.00% X
DeepSeek-RI
100.00% /
0.00% X
Table 18: Redis Raft
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-
100.00%
0.00%
GPT-5
100.00% /
0.00% x
Basic Modeling
Gemini-2.5-Pe
50.00% X
DeepSeck-RI
100.00%
0.00%
Claude-Sonnet-4
100.00% /
23.81% /
9.09%
75.00%
GPT-5
100.00% /
0.00%
Code Translation
Gemini-2.5-B Pro
50.00% X
DeepSeck-RR R1
100.00% /
100.00% /
0.00%
25.00%
Claude-Sonnet-4
50.00%
GPT-5
47.06% X
Trace Learning
Gemini-2.5-PP
100.00% /
0.00% X
DeepSeek-RI
48.53%
The system model generated by DeepSeek-RI is overly simplified; thus, has high syntax and runtime correctness, has low score on invariants (the protocol logic incorrect) and 0% on conformance.
35

---

Published as a conference paper at ICLR 2026
Table 19: Xline CURP
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00% /
0.00% x
GPT-5
100.00% /
0.00% x
Basic Modeling
Demini-2.5-Par
100.00% /
0.00%
DeepSeek-RR
100.00%
0.00%
Claude-Sonnet-4
100.00% /
100.00% /
50.00%
100.00%
GPT-5
100.00%
0.00%
Code Translation
Gemini-2.5-PP Pro-
100.00% /
100.00% /
66.67%
100.00%
DecpSeek-RI
100.00%
0.00% X
Claude-Sonnet-4
50.00% X
GPT-5
100.00% /
0.00% X
Trace Learning
Gemini-2.5-Por
46.15% X
DeepSeck-RI
100.00% /
0.00%
Xline CURP is of the largest system artifacts in SYSMOBENCH Table I. We suspect that the system
model generated by Gemini-2.55PP benefits from 1M- (M-token context window, enabling effective summarization of the 4000+ line codebase into a concise TLA* representation.
Table 20: PGo dqueue
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00%
33.33%
33.33%
0.00%
GPT-5
100.00%
0.00%
Basic Modeling
Gemini-2.5-Pra
100.00%
0.00%
DeepSeck-RI
100.00% /
0.00%
Claude-Sonnet-4
100.00%
100.00% /
0.00%
100.00%
GPT-5
100.00% /
100.00% /
0.00%
100.00%
Code Translation
Gemini-2.55PP5
100.00%
100.00% V
0.00%
100.00%
DeepSeek-R1
100.00%
100.00% /
0.00%
100.00%
Claude-Sonnets
100.00%
0.00%
GPT-5
100.00%
0.00%
Trace Learning
Gemini-2.5-PP5
100.00% /
0.00%
DeepSeek-RI
100.00% /
0.00%
Table 21: PGo locksve
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonet-4 GPT-5
44.45%
100.00% /
0.00% X
Basic Modeling
Gemini-2.5-Pro
100.00% /
0.00% x
DeepSeck-Rl R1
100.00% /
0.00% X
Claude-Sonnet-4
100.00% /
100.00% /
0.00%
83.33%
GPT-5
100.00% /
100.00% /
0.00%
66.67%
Code Translation
Gemini-2.5-PP
100.00%
0.00%
DeepSeek-RR -1
100.00%
100.00% /
0.00%
50.00%
Claude-Sonnet-4
42.31%
GPT-5
100.00%
0.00% X
Trace Learning
Gemini-2.5-4 Pro-rro
50.00% X
DeepSeek-RI
50.00% X
36

---

Published as a conference paper at ICLR 2026
Table 22: PGo raftkvs
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
44.57% X
GPT-5
100.00% /
0.00% x
Basic Modeling
Gemini-2.5-Pro
45.84% X
DeepSeck-RI
45.32%
Claude-Sonnct-4
100.00% /
50.00% /
0.00%
90.91%
GPT-5
100.00% /
100.00% /
0.00%
72.73%
Code Translation
Gemini-2.5-Pot
40.91% X
DeepSeek-RI
100.00% /
22.22% x
Claude-Sonnet-
50.00% X
GPT-5
46.55% X
Trace Learning
Gemini-2.5-Po5
41.67% X
DeepSeck-R1 47.83%
We observe that the characteristics LLM performance on PGo-compiled systems very different from Huiman-writtee systems as discussed in Section SectionSJand Appendix [ find that GPT-5 generally performs well on PGo systems, indicating its ability of understanding machine-generatee code patterns.
Table 23: ZooKeeper Fast Leader Election (FLE)
Agent
LLM
Syntax
Runtime
Conformance
Invariant
Claude-Sonnet-4
100.00%
0.00%
GPT-5
100.00%
0.00%
Basic Modeling
Gemini-2.5-Pro
100.00% /
0.00%
DeepSeek-RI R1
100.00% /
0.00% X
Claude-Sonnet-4
100.00% /
0.00% x
GPT-S
100.00% /
0.00% X
Code Translation
Gemini-2.5-Pro
100.00% /
0.00%
DeepSeck-RI
100.00% /
0.00%
Claude-Sonnet-4
44.44%
GPT-5
47.92%
Trace Learning
Gemini-2.5-PP
100.00% /
0.00%
DeepSeek-RI 100.00% /
0.00% X
ZooKeeper FLE has the largest codebase and implements the complex ZAB protocol, making the most challenging system to model among all eleven artifacts.
37


Reviews:
[{"review_id": "VDva2Fl2QL", "reviewer": "Reviewer_f1Je", "summary": "This paper presents a new benchmark, SysMoBench, for assessing the ability of AI systems to generate valid formal models of complex real-world systems. The main contributions of the paper are threefold:\n1. The authors properly define key metrics to assess the quality of the AI generated system models (based on syntax correctness, runtime correctness, conformance to the system implementation and invariant correctness)\n2. The authors also clearly lay out an effective fully automated approach to compute those metrics \n3. An empirical evaluation that shows the limitation of state-of-the-art LLMs in generating system models for real-world complex systems.", "questions": "The authors write in section 3.2.4: \n>\"In principle, if a system model fully conforms to code, violations of these invariants would indicate bugs in system code; in practice, few\nAI-generated models achieved fine-grained conformance.\"\n\nLet's assume that, with the help of this new benchmark, state-of-the-art LLMs improve significantly at complex system modeling tasks. What approach would you recommend to determine whether a violation of an invariant stems from a rare LLM modeling error or from an actual bug in the system code?", "limitations": "", "rating": 8, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 4, "strengths": "1. **Relevance**\nThe paper addresses a critical challenge: evaluating the capability of AI systems to move beyond basic code generation and comprehension, toward a deeper understanding and modeling of complex real-world systems.\n\n2. **Significance and Novelty**\nTo the best of my knowledge, the proposed approach is novel in its problem formulation, the techniques used to fully automate the quality assessment of AI-generated models, and its focus on real-world complex systems. The introduction of this new benchmark holds strong potential for significant impact, as it provides a vital resource that could accelerate progress in AI-driven modeling of complex systems.\n\n3. **Soundness and Experimental Evaluation**\nThe experimental results validate the effectiveness and robustness of the key LLM-assisted components within the automated evaluation pipeline. They also highlight that current state-of-the-art LLMs still face challenges in accurately modeling complex real-world systems, which underscores the importance of this benchmark in advancing research on AI modeling of intricate software systems.", "weaknesses": "I could not find any major problem with the paper.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "t6jbaorvBi", "reviewer": "Reviewer_Sb7c", "summary": "This paper introduces SysMoBench, which is a benchmark framework for evaluating the outputs of large language models using a formal specification language called TLA^{+}. The authors developed nine benchmarks and evaluated the types of syntax and runtime errors, as well as violations of safety and liveness specifications. The authors evaluate the frontier models by expressing them using TLA^{+} language outputs.", "questions": "The authors listed a number of benchmarks, such as MMLU, ARC, and HELM, but I think there's a lack of motivation behind using TLA^{+}. There are also some comparisons missing relevant to structured reasoning, such as EvalScope and Agent-SafetyBench. I would like to understand why using TLA^{+} is a much better alternative than these benchmarks, considering that it's not a very common specification language, such as linear temporal logic. The authors should also spend some time on defining the basic properties of TLA^{+}.\n\nI think it's also unclear how the benchmark tasks were generated, and how this tool can be extended to use different benchmarks. The authors mention this in a paragraph, but I don't see the point of adding their subjective experience without an extensive introduction in the appendix.", "limitations": "", "rating": 2, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "The authors develop a benchmarking tool to evaluate LLM outputs with tools from formal methods, and using a formal specification language. The benchmark also evaluates several types of errors, such as syntax and runtime errors, as well as violations of safety and liveness specifications.", "weaknesses": "I think the benchmarks in the paper mainly demonstrate the lack of capability of outputting TLA^{+} models for these models, which is mentioned in the \"Analysis on LLMs\". I think that the reason Claude-sonnet is overperforming is mainly because it's more adept at creating outputs with TLA^{+} syntax, but not necessarily having a superior ability to reason and generate real-world system artifacts.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "vGfnzd0jKi", "reviewer": "Reviewer_K1Um", "summary": "The paper introduces SYSMOBENCH, a benchmark designed to evaluate generative AI (LLMs and agents) on their ability to formally model complex real-world systems, particularly concurrent and distributed ones.\nUsing TLA+ as the modeling language, the benchmark assesses how well AI can synthesize system-level formal specifications from code, documentation, and execution traces.\n\nSYSMOBENCH defines four automatic evaluation metrics and provides tasks from nine real-world system artifacts (e.g., Etcd Raft, Redis Raft, Asterinas OS spinlock/mutex).\nExperiments with four LLMs (Claude-Sonnet-4, GPT-5, Gemini-2.5-Pro, DeepSeek-R1) and three agent designs show that AI can handle simple concurrency models (e.g., spinlocks) but fails on large-scale distributed systems (e.g., Raft).", "questions": "How easy is it to extend SYSMOBENCH to other formal languages (e.g., Alloy, PAT)? A discussion on generalization beyond TLA+ would make the benchmark more widely applicable.\n\nThe authors note that LLMs often fail on liveness invariants. Could they provide finer-grained analysis (e.g., which temporal operators or fairness conditions are most misunderstood)?\n\nCan SYSMOBENCH-produced AI-generated models be useful to human engineers (e.g., partial correctness checking or documentation)? Some qualitative human evaluation would strengthen its practical impact.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "- Novel Benchmark and Scope\n\nFocusing on system-level formal modeling, going beyond prior works on function-level specification or toy TLA+ examples.\n\n- Automatic and Quantitative Evaluation Metrics\n\nProposes a clear, reproducible metric suite (syntax, runtime, conformance, invariant) for assessing AI-generated TLA+ models without human involvement.\n\n- Empirical and Realistic Evaluation\n\nUses real-world system artifacts (Etcd, Redis, Asterinas, etc.), showing the practical limitations of current LLMs and agents in understanding and abstracting complex system behaviors.", "weaknesses": "- Shallow Semantic Understanding\n\nThe current metrics emphasize syntactic, runtime, and invariant correctness, but do not directly measure whether AI truly captures the semantic intent or design rationale of the system.\n\n- Lack of Human Baseline Comparison\n\nNo comparison with expert-written TLA+ specifications is provided. Without a human reference, it is hard to assess how “good” the AI-generated models truly are in abstraction quality or maintainability.\n\n- Limited Scalability\n\nAdding a new system using LLM still requires 3–4 days of human setup (instrumentation, trace harness preparation), which challenges scalability despite claims of automation. \n\n- Risk of Contamination and Overfitting\n\nSome system code (e.g., Etcd Raft) may already appear in LLM training data, possibly affecting fairness; the paper lacks a clear anti-contamination discussion.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "lxNJjw9oEL", "reviewer": "Reviewer_RwMC", "summary": "In this work, the authors propose a benchmark dataset for evaluating LLMs in terms of their capability of system modelling. The dataset contains 9 systems/models, and the authors propose 4 different metrics for evaluating the quality of the model constructed by the LLMs. Some empirical results are then presented.", "questions": "If the AI uses different data-structures (one-dimensional list instead of two-dimensional one) or different encoding to model the same action,  can you tell that it is correct?", "limitations": "", "rating": 2, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "On the positive side, I enjoy reading the draft for the following reasons.\n\nFirst, the problem of evaluating LLMs capability of system modeling, which can be regarded as one particular form of abstract thinking capability, is an interesting and important one.\n\nSecond, the idea of evaluating the quality of the models at different levels is a valid idea.\n\nLastly, the writing is easy to follow and some of the empirical results are interesting.", "weaknesses": "On the less positive side, the draft can be improved from the following aspects.\n\nFirst, the benchmark data is fairly small in size and lacks variety (i.e., only one modeling language), and there is not a very interesting or useful benchmark yet. More importantly, it seems to be rather hard to scale up the dataset as well.\n\nSecond, the proposed ways of measuring the quality of the model can be much improved, and much details on how exactly the scoring is done is missing. For instance, for per-action specification, it is not clear how a specification is considered correct - do you have to check specification equivalence, modular renaming, using different data structures and so on? \n\nThe following are a list of detailed comments.\n\nPage 2: “SYSMOBENCH currently includes a diverse set of nine real-world artifacts, …”\n\nComment: The size of the benchmark set raises questions on whether such a benchmark set would produce statistically significant evaluating results. \n\nPage 2: “SYSMOBENCH enables us to understand the capabilities and limitations of AI in modeling realworld\nsystems by evaluating different agent designs with various AI models.”\n\nComment: Given that only one modelling language is evaluated, this statement is rather an over-statement. \n\nSection 3.1: line 183-190\n\nComment: It is rather arguable whether such a modeling requirement is reasonable or. In practice, the level of details to be included in the model typically depends on the analysis task. i.e., the properties to be established or falsified. Simply saying that some actions should be modeled is not sufficient as there are many ways of modeling the same action.\n\nPage 5: “It then uses SANY to check the per-action specification.”\n\nComment: How is this done? In general, this boils down to a specification equivalence checking which is hard.\n\nPage 9: “For example, adding Etcd Raft took one SYSMOBENCH author four days; an Xline CURP contributor with no experience of SYSMOBENCH added the system to SYSMOBENCH in four days.”\n\nComment: Four days per mode is not exactly efficient. Furthermore, there are questions such as who decides the model is correct? Lastly, if four man/day is all that is needed for one model, why are there only 9 in total?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)