Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems

Qian Cheng, Ruize Tang, Emilie Ma, Finn Hackett, Peiyang He, Yiming Su, Ivan Beschastnikh, Yu Huang, Xiaoxing Ma, Tianyin Xu

TL;DR

SysMoBench tackles the challenge of evaluating AI-generated formal models for large, real-world distributed systems by adopting the TLA+ language and an automated metric pipeline. It defines four core metrics—syntax correctness, runtime correctness, conformance, and invariant correctness—and demonstrates an end-to-end workflow from task specification to automated checks. Results on Spinlock and Etcd Raft reveal that while current LLMs can model small artifacts, large, protocol-rich systems remain difficult, though code-translation approaches can improve coverage and correctness. The benchmark provides a foundation for advancing AI-assisted formal modeling, with implications for maintaining correct, scalable system specifications in production environments.

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 code, 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 computing infrastructures, encompassing operating systems and cloud infrastructure. We use TLA+, the de facto specification language for concurrent and distributed systems, though the benchmark can be extended to other specification 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 nine diverse system artifacts: the Raft implementation of Etcd and Redis, the Spinlock and Mutex in Asterinas OS, etc.; more artifacts are being actively added. SysMoBench enables us to understand the capabilities and limitations of today's LLMs and agents, putting tools in this area on a firm footing and opening up promising new research directions.

SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems

TL;DR

SysMoBench tackles the challenge of evaluating AI-generated formal models for large, real-world distributed systems by adopting the TLA+ language and an automated metric pipeline. It defines four core metrics—syntax correctness, runtime correctness, conformance, and invariant correctness—and demonstrates an end-to-end workflow from task specification to automated checks. Results on Spinlock and Etcd Raft reveal that while current LLMs can model small artifacts, large, protocol-rich systems remain difficult, though code-translation approaches can improve coverage and correctness. The benchmark provides a foundation for advancing AI-assisted formal modeling, with implications for maintaining correct, scalable system specifications in production environments.

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 code, 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 computing infrastructures, encompassing operating systems and cloud infrastructure. We use TLA+, the de facto specification language for concurrent and distributed systems, though the benchmark can be extended to other specification 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 nine diverse system artifacts: the Raft implementation of Etcd and Redis, the Spinlock and Mutex in Asterinas OS, etc.; more artifacts are being actively added. SysMoBench enables us to understand the capabilities and limitations of today's LLMs and agents, putting tools in this area on a firm footing and opening up promising new research directions.

Paper Structure

This paper contains 27 sections, 4 figures, 12 tables.

Table of Contents

  1. Introduction
  2. Background
  3. SysMoBench
  4. Task Formulation
  5. Metrics and Their Measurement
  6. Syntax Correctness
  7. Runtime Correctness
  8. Conformance to System implementation
  9. Invariant Correctness
  10. Adding New Systems to SysMoBench
  11. Evaluation Setup
  12. Results
  13. Related Work
  14. Concluding Remarks
  15. Alternative Metrics
  16. ...and 12 more sections

Figures (4)

  • Figure 1: SysMoBench sources its tasks from real-world systems (e.g., Etcd Raft in the figure). It automatically evaluates the system models in TLA$^+$ generated by AI with different metrics.
  • Figure 2: Simplified code that implements a spinlock in Asterinas (left) and an AI-generated TLA$^+$ model (right). A spinlock represents the simplest system in SysMoBench.
  • Figure 3: 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 4: LLM error attribution regarding the SysMoBench metrics in the basic modeling agent. The conformance metric is omitted as it has a single attribution.