SpecMAS: A Multi-Agent System for Self-Verifying System Generation via Formal Model Checking¶

🕒 Published (v1): 2025-01-01 · Source: NeurIPS · Venue: NeurIPS 2025 · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

SpecMAS is a multi-agent system that autonomously synthesizes and formally verifies executable NuSMV models from natural language Standard Operating Procedures (SOPs) using a closed-loop pipeline of Kripke model generation, CTL/LTL property extraction, symbolic model checking, and counterexample-guided self-correction. The system achieves the highest Final Compliance Score on 4 of 5 MiniSpecBench benchmarks, outperforming Claude 3.7-Sonnet, DeepSeek-R1, Gemini Flash-2.5, and Qwen3-235B.

Problem¶

Formal model checking of complex systems requires expert-crafted NuSMV models and property specifications—a bottleneck that prevents deployment in mission-critical domains where AI-generated systems lack accessible test suites or expert-defined correctness criteria. Prior LLM-assisted approaches are domain-specific, perform post-hoc verification only, omit transition models, or lack automated debugging of counterexamples.

Method¶

SpecMAS operates as two tightly-coupled agentic pipelines:

Pipeline I – Model & Specification Synthesis: An information-gathering agent parses SOP documents (augmented via SCMRAG retrieval), a Kripke Extractor agent constructs the finite-state transition system M = ⟨S, S₀, R, L⟩, and a Property Extractor agent derives both explicit SOP requirements and implicit properties (invariants, liveness, safety) via semantic reasoning and a ReACT-style solver. Both artifacts are serialized to NuSMV .smv format.

Pipeline II – Model-Checking & Debugging: The NuSMV symbolic model checker executes the model. On failure, a dedicated Debugging Agent classifies the error (syntax, counterexample, or unsupported semantics) and iteratively patches the model or property set using the full revision history as context. The loop repeats until M |= φ for all properties. The backbone LLM is an 8-bit quantized Qwen3-32B.

Key Contributions¶

End-to-end pipeline from natural language SOP to machine-verified NuSMV model with formal correctness guarantee by construction
Property exploration agent that extracts both explicit and implicit CTL/LTL specifications from unstructured text
Counterexample-guided debugging agent that interprets LTL (αβω) and CTL (finite path with falsified sub-formula annotations) traces to iteratively repair models
MiniSpecBench: 10 SOP–NuSMV paired documents covering industrial motifs (BRP protocol, shuttle autopilot, mutual exclusion, robot controller, cache coherence), with SOPs auto-generated via SYNTHIA from canonical NuSMV examples
Ablation confirming that the integrated verification-debugging loop (not LLM synthesis alone) drives compliance gains

Results¶

Evaluated on 5 MiniSpecBench systems via LLM-as-a-Judge across Structural Alignment, Property Fidelity, Semantic Fidelity, Code Compliance, and Execution Compliance (Final = 40% Code + 60% Execution):

SpecMAS achieves highest Final Compliance Score on 4/5 systems: BRP (0.76), Shuttle Autopilot (0.76), Robot Controller (0.69), GigaMax Cache (0.70); Mutual Exclusion (0.77, best among all)
Execution Compliance dominance: SpecMAS reaches 0.90 on BRP vs. Claude 0.38, Gemini 0.0*, Qwen 0.16; 0.97 on Shuttle Autopilot vs. next-best Gemini 0.60; 0.90 on Robot Controller vs. DeepSeek 0.64 (Claude, Gemini, Qwen all fail to execute)
Gemini Flash-2.5 fails to produce executable models on 3/5 tasks; Qwen3-235B underperforms despite 7× more parameters than SpecMAS's Qwen3-32B
Debug steps vs. quality tradeoff: DeepSeek requires 0–2 manual fixes but achieves low compliance; SpecMAS requires 3–7 agent-led iterations yet achieves substantially higher final scores (e.g., +0.39 on Robot Controller vs. Claude's 1-step baseline)
Ablation: synthesis-only pipeline (no debugging loop) frequently fails execution; full pipeline recovers even cases with missed state transitions (Mutual Exclusion)

Limitations¶

Benchmark SOPs are auto-generated from NuSMV code via SYNTHIA, not human-authored; robustness to natural linguistic variability is untested
NuSMV restriction precludes direct modeling of hybrid or probabilistic systems; continuous behavior requires discrete abstraction
State-space explosion in high-complexity systems can increase debugging iterations (avg. ~18 additional steps on hardest tasks)
Extreme SOP ambiguity may still require human-in-the-loop assistance despite RAG-based inference
Some verified properties may not fully capture intended operational semantics despite entailment classification

Relevance to Agentic AI / LLM Agents¶

SpecMAS exemplifies a core pattern in agentic AI: using tool-augmented, multi-agent closed-loop feedback to achieve formal correctness that one-shot LLM generation cannot guarantee. The counterexample-guided self-repair loop is a concrete instantiation of the "plan-execute-observe-revise" agentic cycle applied to a domain (formal verification) where correctness is objectively decidable—making it a strong testbed for agent reliability. The finding that syntactically clean one-shot outputs (DeepSeek, Qwen) systematically fail execution while iterative agentic correction produces high-compliance artifacts directly challenges the sufficiency of single-pass generation for safety-critical code synthesis. This connects to broader work on self-debugging agents, LLM-guided formal methods, and the need for execution-grounded evaluation rather than surface-level code quality scores.