TLDR: SYSMOBENCH is a new benchmark that evaluates how well AI, particularly large language models and agents, can create formal models for complex real-world computer systems like distributed protocols and operating system components. It introduces automated metrics for syntax, runtime, conformance, and invariant correctness, revealing that while AI can model simpler systems, it struggles with the complexity and abstraction required for larger systems. The study found that code translation approaches show more promise than direct modeling or trace learning, and LLMs generally struggle more with liveness properties than safety properties.
The world of complex computer systems, especially those that are concurrent and distributed, relies heavily on formal models to ensure their correctness and reliability. These models provide a mathematical blueprint for how a system should behave, allowing developers to verify its design and implementation. However, creating and maintaining these formal models is notoriously difficult and expensive, often requiring specialized expertise and significant time.
Recent advancements in generative AI, particularly large language models (LLMs) and agentic techniques, have shown potential in generating various forms of software specifications. Yet, most existing work has focused on smaller code segments, leaving a crucial question unanswered: Can AI effectively model entire, complex real-world systems? This challenge requires AI to not only understand intricate behavioral properties but also abstract them into precise formal models.
Introducing SYSMOBENCH: A New Benchmark for AI System Modeling
To address this gap, researchers have introduced SYSMOBENCH, a groundbreaking benchmark designed to evaluate AI’s capability in formally modeling large and complex systems. The benchmark specifically targets concurrent and distributed systems, which form the backbone of today’s critical computing infrastructure, including operating systems and cloud services. SYSMOBENCH utilizes TLA+, a widely recognized specification language for these types of systems, though its framework is adaptable to other languages.
A core innovation of SYSMOBENCH lies in its automated evaluation metrics, which overcome the limitations of manual assessment. These metrics provide a robust way to gauge the quality of AI-generated models:
-
Syntax Correctness: Checks if the generated TLA+ model adheres to valid syntax rules using the SANY Syntactic Analyzer. This includes both full-model and per-action syntax checks.
-
Runtime Correctness: Evaluates if the model can be executed correctly using the TLC model checker, acting as a proxy for logical self-consistency and identifying runtime errors during state space exploration.
-
Conformance to System Implementation: Measures how well the model’s behavior aligns with the actual system code through trace validation. This involves instrumenting system code to collect execution traces and mapping them to the model’s state space.
-
Invariant Correctness: Determines if the AI-generated models consistently satisfy predefined safety and liveness properties (invariants) of the system, using model checking to detect violations.
SYSMOBENCH currently features nine diverse real-world system artifacts, including distributed consensus systems like the Raft implementations in Etcd and Redis, and concurrent mechanisms such as Spinlock and Mutex from the Asterinas operating system. The benchmark is continuously expanding with more artifacts.
How AI Agents Perform
The research evaluated three types of AI agents powered by various LLMs, including Claude-Sonnet-4, GPT-5, Gemini-2.5-Pro, and DeepSeek-R1:
-
Basic Modeling Agent: Directly prompts an LLM with source code and task requirements.
-
Code Translation Agent: Uses an LLM to translate code statement-by-statement into TLA+.
-
Trace Learning Agent: Attempts to infer system models directly from runtime traces.
The findings reveal a nuanced picture of current AI capabilities. For simpler systems like the Asterinas Spinlock, basic modeling agents demonstrated good performance, generating high-quality TLA+ models. However, when faced with larger and more complex distributed protocols, such as Etcd Raft, these agents struggled significantly. Challenges included the sheer verbosity of the code, the inherent complexity of the protocols, and the difficulty in abstracting high-level system behaviors into formal TLA+ constructs.
Interestingly, the code translation agent showed better performance for complex systems. This suggests that leveraging LLMs’ ability to translate code, combined with symbolic control-flow analysis, can be a more effective strategy for model generation. In contrast, the trace learning agent generally underperformed, often failing basic compilation and runtime checks.
The study also highlighted specific strengths and weaknesses among the LLMs. Claude-Sonnet-4, for instance, generally produced TLA+ models with more correct syntax compared to others, which frequently introduced errors like misusing mathematical symbols or mixing TLA+ syntax with other programming languages. Furthermore, LLMs showed a greater tendency to violate liveness properties (which concern eventual outcomes) than safety properties (which concern undesirable states), indicating limitations in temporal reasoning.
Also Read:
- Advancing Software Verification: New Tools for Large-Scale Codebases
- LLM Agents Tackle Real-World Software Compilation Challenges with BUILD-BENCH
The Path Forward
SYSMOBENCH represents a significant step towards understanding and advancing AI’s role in formal system modeling. By providing a rigorous and automated evaluation framework, it helps identify the current capabilities and limitations of generative AI in this critical domain. The benchmark aims to spur new research directions, pushing AI technologies beyond mere code intelligence towards a deeper understanding and formal specification of complex software systems. For more details, you can refer to the full research paper here.
