Technical Summary: SYSMOBENCH

Problem Statement

Formal models are critical for specifying and verifying the correctness of large, complex computer systems, particularly in the domains of distributed and concurrent computing. However, creating these models is notoriously expensive, requiring significant expert effort to abstract low-level system code into rigorous mathematical specifications. While recent advances in generative AI (LLMs and agentic techniques) have shown promise in generating function-level specifications (e.g., pre- and post-conditions), it remains unclear whether AI can effectively model complete, real-world systems. Existing benchmarks primarily target small code snippets or logic puzzles, failing to address the complexities of abstracting system design, reasoning about safety and liveness under faults, and handling the scale of production-grade artifacts.

Methodology

The authors present SYSMOBENCH, a benchmark designed to evaluate the ability of generative AI to formally model complex real-world systems. The framework focuses on concurrent and distributed systems, which underpin critical infrastructure like operating systems and cloud services.

Core Components

1. Task Formulation: The benchmark tasks AI agents to generate formal system models (specifically in TLA+, the de facto specification language for such systems) from real-world system artifacts. The input includes source code, documentation, and runtime traces. The output must capture essential behavioral properties and state transitions while excluding irrelevant implementation details.
2. System Artifacts: The benchmark currently includes eleven diverse artifacts, ranging from simple synchronization primitives (Spinlock, Mutex, Ringbuffer in the Asterinas OS) to complex distributed protocols (Etcd Raft, Redis Raft, ZooKeeper FLE, Xline CURP) and compiler-generated systems (PGo).
3. Automated Evaluation Metrics: A key contribution is the development of automated, quantitative metrics to assess model quality without relying on brittle human comparison or "LLM-as-a-judge" approaches. The metrics include:
   • Syntax Correctness: Validated using the SANY Syntactic Analyzer. It employs a weighted scoring scheme (full-model vs. per-action) to handle partial correctness.
   • Runtime Correctness: Measured by the fraction of model actions that can be executed without errors using the TLC model checker, serving as a proxy for logical self-consistency.
   • Conformance: Assessed via trace validation, where execution traces from the instrumented system code are checked against the generated model's state space. This involves using an LLM to map model elements to code elements to handle naming discrepancies.
   • Invariant Correctness: Evaluates whether the model satisfies system-specific safety and liveness properties. Invariant templates are concretized into model-specific TLA+ formulas using LLMs and then verified via model checking.

Evaluation Agents

The study evaluates three distinct agent designs powered by four state-of-the-art LLMs (Claude-Sonnet-4, GPT-5, Gemini-2.5-Pro, DeepSeek-R1):

• Basic Modeling Agent: Prompts the LLM directly with source code and task requirements.
• Code Translation Agent: Translates system code statement-by-statement into TLA+ before organizing control flows.
• Trace Learning Agent: Infers the system model solely from runtime traces without code input.

Key Results

The evaluation reveals significant limitations in current AI capabilities regarding complex system modeling:

• Scalability Gap: AI agents perform well on small, simple artifacts (e.g., Asterinas Spinlock), often achieving high scores in syntax, runtime, and conformance. However, performance degrades sharply on larger, complex systems like Etcd Raft. For instance, on Etcd Raft, even the best-performing agent (Claude-Sonnet-4 with code translation) achieved only 15.38% conformance and 92.31% invariant correctness, while other agents failed to pass syntax or runtime checks entirely.
• Abstraction Challenges: The primary failure modes for complex systems include difficulty handling code verbosity, understanding intricate protocol logic (e.g., Raft ordering), and correctly abstracting nested data structures (e.g., distributed logs).
• Agent Performance: The Code Translation Agent generally outperformed the Basic Modeling Agent on complex systems, suggesting that leveraging LLMs' code translation capabilities helps prevent hallucination of logic. The Trace Learning Agent performed poorly across the board, often failing compilation and runtime checks, indicating that inferring system models from traces is currently more difficult for LLMs than processing source code.
• Error Analysis: Syntax errors are frequent, particularly with mathematical symbols and operator misuse. Runtime errors often stem from inconsistent configurations or misunderstandings of TLA+ data structures. Notably, LLMs struggle significantly with liveness properties, with 41.9% of invariant violations related to liveness compared to only 8.3% for safety properties, highlighting a weakness in temporal reasoning.
• Qualitative Utility: Despite quantitative limitations, AI-generated models successfully reproduced known bugs in five different systems, demonstrating practical utility for partial correctness checking.

Significance and Claims

The authors position SYSMOBENCH as a foundational step toward advancing AI from "code intelligence" to "system intelligence."

• Benchmarking Reality: The paper claims that while AI shows promise in coding tasks, it currently lacks the capability to comprehend, abstract, and specify large, complex systems required for formal verification.
• Automated Evaluation: By establishing automated metrics for syntax, runtime, conformance, and invariants, SYSMOBENCH provides a scalable and objective way to measure progress in this domain, moving beyond the limitations of existing benchmarks that focus on small programs or logic puzzles.
• Future Direction: The authors view SYSMOBENCH as a vehicle to spur innovative AI approaches. They note that the benchmark is extensible (supporting Alloy and PAT) and actively expanding its artifact collection. They emphasize that the goal is not merely to generate code but to enable AI to assist in the formal verification of safety-critical real-world systems, similar to the role SWE-bench plays in software engineering.

The paper concludes that current LLMs are limited in modeling complex systems but that the framework provides the necessary tools to track improvements and guide the development of more capable AI agents for formal system modeling.