SpecMAS: A Multi-Agent System for Self-Verifying System Generation via Formal Model Checking
Authors: Rishabh Agrawal
Kaushik Tushar Ranade
Aja Khanal
Kalyan Shankar Basu
Apurva Narayan
Venue: NeurIPS 2025 poster ()
Keywords: Multi-agent systems
formal verification
temporal logic
specification generation
model-checking
Large Language Models
Primary area: deep_learning
TL;DR: SpecMAS converts natural-language SOPs into NuSMV models and autonomously self-verifies and debugs them via multi-agent temporal-logic checking, ensuring verifiable system designs.

Abstract: We present SpecMAS, a novel multi-agent system that autonomously constructs and formally verifies executable system models from natural language specifications. Given a Standard Operating Procedure (SOP) describing a target system, SpecMAS parses the specification, identifies relevant operational modes, variables, transitions, and properties, and generates a formal model in NuSMV code syntax, an industry-standard symbolic model checker. A dedicated reasoning agent extracts both explicit and implicit properties from the SOP, and verification is performed via temporal logic model checking. If any properties fail to verify, an autonomous debugging agent analyzes counterexamples and iteratively corrects the model until all properties are satisfied. This closed-loop system design guarantees provable correctness by construction and advances the state of the art in automated, interpretable, and deployable verification pipelines. We demonstrate the generality, correctness, and practical feasibility of SpecMAS across a set of representative case studies and propose a new benchmark dataset for the evaluation and comparison of model checking performance.

SpecMAS: A Multi-Agent System for Self- Veef-Veriggnn System Generation via Formal Model Checking
Rishabh Agrawal Kaushik Tushar Ranade Aja Khanal'
Kalyan S. Basu? Apurva Narayan'
'Department of Computer Science, University of Western Ontario, London, Ontario
ICASSSD, Cambridge, Ontario (ragrawa9, kranade, akhanal3, apurva. www.aa..aaaaaanaaaa.a. www.yaaaaauooo..oomoo.. ks. ks.basu@gmail.
Abstract
We present SpecMAS, a novel multi-agent system that autonomously constructs and formally verifies executable system models from natural language specifica- tions. Given a Standard Operating Procedure (SOP) describing a target system, SpecMAS parses the specification, identifies relevant operational modes, variables, transitions. and properties, and generates a formal model in NuSMV code syntax, an industry-standard symbolic model checker. A dedicated reasoning agent extracts both explicit and implicit properties from the SOP, and verification is performed via temporal logic model checking. If any properties fail verify, an autonomous debugging agent analyzes counterexamples and iteratively corrects the model until all properties are satisfied. This closed-loop system design guarantees provable correctness by construction and advances the state of the art in automated, inter- pretable, and deployable verification pipelines. We demonstrate the generality, correctness, and practical feasibility of SpecMAS across set of representative case studies and propose new benchmark dataset for the evaluation and comparison of model checking performance. feituu.coom/dss-groop///
We release code and benchmark dataset
Introduction
The increasing complexity and autonomy of modern software systems have made it critical to develop frameworks that not only generate such systems from specifications but also provide formal guarantees about their behavior. Formal specifications define pre-Ipost-conditions, invariants, and other assertions that must hold throughout system execution 2 In mission-critical domains such healthcare, aviation, and industrial automation, informal reasoning and empirical testing enough 4]. This is especially true when Al agents are use to generate and execute the system. In such cases, proper testing suite or expert-defined system properties may be available to verify correctness of the system while it is being generated (5). This necessitates approaches that integrate both system synthesis and formal verification in closed-loop manner.
In this paper, we propose SpecMAS, a novel multi-agent framework that autonomously ingests system specifications in the form of Standard Operating Procedure (SOP) and constructs complete formal system model using temporal logic and symbolic representations (via NuSMV [6]). We extract system states, transitions, and property specifications, and systematically verify their correctness using model checking 7 To ensure comprehensive verification, our framework includes a dedicated reasoning agent [8] that identifies and encodes all properties. Explicit properties are directly extracted from the SOP, while implicit ones are inferred through a property exploration process driven by semantic analysis and contextual reasoning. If any specification properties fail during verification,
"Equal Contribution
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

our system leverages a dedicated Model Checker Debugging Agent that interprets counterexample traces to iteratively revise and correct the system model or properties until all generated specifications pass verification checks.
1.1 Objectives and Contributions
1. Automated Model Synthesis: Design a multi- system capable of extracting operational modes, variables, and transitions from natural language SOPs and translating them into formal NuSMV models.
2. End-to-End Formal Verification: Use symbolic model checking to ensure that all temporal logic properties (c.g., invariants, safety, reachability) are satisfied by the synthesized model.
3. Recursive Self-Correction: Introduce an agentic feedback loop that interprets NuSMV coun- terexamples and autonomously revises faulty specifications or transitions until full verification is achieved.
Provide a foundation for building agentic systems that are correct by construction, thus bridging AI generated systems with formal logic and safety.
Theoretical Guarantees:
5. Scalability and Generality: Demonstrate the generalisability of SpecMAS across diverse domains through empirical validation and analysis MiniSpecBench dataset with both synthetic and expert- designed formal models.
A key contribution of SpecMAS is its direct use of NuSMV, industry -standadd tool for symbolic model checking. Unlike prior work that relies on custom languages or proprietary compilers, our framework generates models in NuSMV's native specification language, enabling seamless integration with existing verification toolchains. This design choice reduces adoption barriers, eliminates the need for custom infrastructure, and leverages mature ecosystem with robust support for temporal logic, counterexample generation, and scalability, By merging model synthesis, formal verification, and self-correction within a unified multi-agent framework, SpecMAS represents a step toward trustworthy autonomous systems capable of reasoning about the correctness of their own design.
2 Previous Work
Model checking is formal verification technique that systematically explores the state space of system model to determine whether it satisfies specified properties, typically expressed in temporal logic such as Computation Tree Logic (CTL) or Linear Temporal Logic (LTL). It has been widely adopted in safety-critical domains due to its ability to provide exhaustive guarantees about system behavior under all possible execution paths. Tools like NuSMV have established themselves as industry standards by offering symbolic and explicit-state verification capabilities. However, despite its rigor, model checking traditionally manual process that requires expert knowledge to construct accurate models and formal specifications. Recent research has explored automating parts of the process but poses significant barrier to scalability and real-world deployment.
2.1 Model Translation and DSL-Based Methods
Several model translation and domain-specific language (DSL) approaches have been proposed to facilitate formal verification. Preibusch and Kammüller 99] presented a framework for translating Object-Z specifications to SMV, preserving object-oriented behavior but requiring manual speci- fication. Zhongsheng et al. [10] compared SPIN, UPPAAL, and NuSMV, finding NuSMV more suited for distributed systems due to its support for CTL and L.TI.. DSL -base methods like MoSt 7 and NL.CCTI. [1T] improve model structure by translating annotated natural language inputs into temporal logic, though they rely on structured inputs or synthetic datasets. Liu et al. [12 introduced Property Specification Language (PSL) tailored to smart contracts, offering formal rule generation but with limited generalizability. While these methods enhance automation and clarity, they are often domain-specific and depend on controlled input formats or prior modeling expertise.
2.2 LLM-Assisted Specification Synthesis and Verification
Wen et al. [3] introduced AutoSpec, a hybrid framework combining static analysis and program verification with LLMdbased specification generation. The system incrementally synthesizes pre-

---

Table 1: Addressing limitations of prior work with the proposed SpecMAS method.
Limitation Category
SpecMAS Solution
Fragmented Scope
Integrates system model generation, property extrac- tion, and recursive verification into single multi-agent pipeline.
Domain Lock-in
Designed to Nomain-agnostic able to operate across SOPs from various fields (e.g.. manufacturing, logistics, control systems).
Post-hoc Verification
Ensures correctness-be ceytieess-yy-ooossuuutttii by embedding ver- ification directly into the synthesis loop.
No Transition Model
Explicitly constructs full NuSMV transition systems (states, variables, transitions) based on SOPs. Extracts both explicit and implicit properties using rea- soning agents, covering invariants, liveness, and safety conditions.
Shallow Property Coverage
No Debugging or Correction
Includes a self-corrective debugging agent that uses counterexamples iteratively fix unverifiable models. Outputs models in NuSMV, an industry-standard formal language, ensuring transparency and adoption feasibility.
Non-interpretable Outputs
conditions, postconditions, and loop invariants for C programs and validates them using theorem provers. Similarly, Ma et al. (14] presented SpecGen, a two-phase approach for formal specifica- tion generation in Java Modeling Language using LLMs. The first phase engages the LLM in conversational prompt-driven loop, refining outputs based on verifier feedback. When this fails, a second mutation- mechanism generates specification variants, which heuristically selected for verification. SpeeGen outperformed traditional tools [[S] [6] which utilize templates defined by human experts to generate candidate specifications. However, such models are fine-tuned for specific domains (e.g.. C/Java programs, smart contracts), limiting their adaptability.
Loop invariants are critical for verifying programs with iterative behavior, yet generating them remains a long-standing challenge. Wu et al. [17] introduced a neuro-symbolic framework that leverages LLMs to generate candidate invariants in "query-filler-reassembbe loop. Bounded Model Checking (BMC) [8] is used to filter invalid predicates, and surviving clauses are recombined into new invariant candidates. Pirzada et al. [19] proposed novel extension of BMC that replaces loop unrolling with LLM- --geeenerteed invariants, verified using a first-order theorem prover [20]. This method was able to prove correctness for programs that other tools 21 22 failed to verify.
3 Proposed Method
We propose SpecMAS, a multi-agent system that automates the synthesis and verification of formal models from natural language SOP documents describing system. At the core of our framework lies the formal verification of system behavior using model checking, grounded in the semantics of Kripke structures. Formally, we represent the synthesized system as a finite-state transition system (Kripke structure) defined by the tuple:
M L)
(1)
where, S is a finite set of states, So S S is the set of initial states, R S S x S is total transition relation capturing all valid system behaviors, and L 5 - AAP is labeling function mapping each state to a set of atomic propositions that hold in that state. Given temporal logic specification y, the verification task reduces to checking whether the system satisfies the property, denoted as:
M -
(2)
SpecMAS constructs M directly from the SOP by identifying system states, variables, and transition conditions through a structured parsing and reasoning pipeline. Properties yp are either explicitly extracted from the SOP or inferred through a property exploration agent. The model then passed to symbolic model checker (NuSMV), which determines the satisfaction of s. LTL properties are
3

---

interpreted over paths; CTL combines path quantifiers A (for all paths) and E (there exists path) with temporal operators X, G, U.
Input:
Standard Operating Procedure document SOP
Output: Varfine-verified NuSMV model Max
Pipeline I- Kripke Model Specification Synthesis:
begin
// Phase 1 Information Gathering
TaskInfo BETRACTTT..K/NEOORATTONSSSS KB);
end
begin
// Phase Kripke Model Generator
K. f- KRIPKEEXTRACTOR<(TSAnn
K f- KRIPKESOLVER(KC ReACT, KB);
I < SELFCORRECT(K, ReACT);
M raw < SERIALIZETONUSMV(C))
end
begin
// Phase 3 Specification Generator
PROPERTYYXXTRACTOR(SPP KB);
< PROPERTYSOLVER ReACT);
Specs_rawe < SERIALIZESPECS(()):
end
Pipeline Model-Checkingg and Debugging:
M + M_waw, Specs + Specs raw;
RevHist 0
// initial revision history; // coding-debugging loop
repeat
STATUS- Sirified then return (M, Specs)
// all properties satisfied
else STATUS = SyntazError then
(M, Specs) < FIXSYNTAX(M, Specs, Refine, KB, RevHist);
else if STATUS = CounterEzamp le then
(M, Specs) GATHERCONTENT& RENIEEEEEEERRRREEEEEEEEEEE Specs, Plan, Plan,, KB, RevHist);
end
else
// unsupported feature Specs) < FIXSEMANTICS Specs, feedback, KB, RevHist);
end
RevHist + RevHist U {(M, Specs));
until (STATUS, feedback) + RUNNUSMV(M, Specs);
Algorithm 1: SPECMAS End-to-End Generation and Verification
In both Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) model checking, counter- example is a witness path (or tree) that demonstrates why a temporal-logic specification yp is false for Kripke structure M (5, So. R, L). For LTL, the violation is witnessed by infinite ultimately-perion path:
8081 ... 8k ($841 ... Sk+e)
8o
So, (84,8441) R.
whose finite prefix of length & is followed by loop of length f > O; by construction и FLTL -pp Because M finite, every counter- example returned by model checker can be represented this a form, where = ..... and 3 $ $1+4.
For CTL, property failure is shown by finite path:
π = Sp$1 Sm
So E So, (511) E R,
(4)
or, for universal violations, finite tree, that ends in a state sm violating required sub-formula. Each position can be annotated with the set:
F. = {ut E M, / w)
(5)
so the complete counter-example is the pair (TT, Fm)) and the non-empty set F.. pinpoints exactly which obligations are violated. Thus, LTI. counter-example mathematically an ultimately- periodic path a with π -= -i, whereas CTL counter-example is finite, transition-consistent

---

Casherng
Specilcatore
Intell Krppe aaneer
Formulzte Plan
Entract Sistes, Dynamic
Tharsalions
Varab
Intaroo Pigperiis Planner
Extect Properics trm
Picpo ty Solrer
Exeratoor
Solvrr
Self Correction
Extruttr
RoACT
Stundard
Mecceduree
Speoikcationa
Protocols
> Tosk
Plan
Kilkk Mode
NUSMI Mocil File
Pleplan
Information
Operations
Requiremerts
Phoperty Eataaterr
eGenaraa Propertaa
#Cmmgerzz Properia
Knowledge
ReACT
Symbolic Vericcatio
Know edge
rdwn NudlVV
Symboik Nerlicatom
Server
-SOMSAG
-CB1 Stase
Ball Tueekke
Nuctote Model a Spscrlaaions File
(a) NuSMV Model and Specifications Generator Agents
Gather Infomation
Coce Contect
Lood on Brona
Speccieed orea
chacker oode
Suspooriad
Yee
Vanboater
Yes
Cide Revatom
Model Checking
Exurple
No
Sebele
Ve
MoskiChackee Nushtt mak
Nc
Rofine NuBMY
(b) NuSMV model-checker Coding and Debugging Agent
Figure Overview of the SPECMAS framework, consisting of two pipelines: (I) Model and Specification Synthesis, where task information is extracted from the SOP to generate Kripke structure and formal properties; and (II) Model Checker Coding and Debugging, which verifies the synthesized NuSMV model using temporal logic and iteratively refines it based counterexamples or syntax errors until all properties are satisfied.
path (or tree) annotated with the falsified sub- formulas at the point of failure. So, if the verification fails, counter examples are used by the proposed debugging agent to recursively revise the model until the relation M }= up holds for all specified properties, thus ensuring correctness by construction.
3.1 Architecture Overview
As shown in Fig. [ the proposed architecture is organised around two tightly-coupled agentic pipelines. The first, Kripke-Model and Specification Synthesis, processes the raw Standard Oper- ating Procedure (SOP) corpus, extracts states, variables and transitions, and packages the resulting Kripke structure together with automatically derived CTL/LTL properties into two artefacts: smv model file and a companion specification file. This pipeline unfolds over three successive caaisessInfomaatiiin Gathering. Kripke Model Generation, and Specification Generation. Through- out these phases every agent can query a shared knowledge base for retrieval-ane vetrieval-augmennedd prompts and invoke a reasoning L.LM that performs on-the-fly symbolic checks, validating both the global plan and the intermediate outputs of each task.
The second pipeline, Model-Checking and Debugging, takes these intermediate artefacts as input, executes the NuSMV engine, and inspects any syntax errors or counter-exampll traces that NuSMV returns. Guided by this feedback, the pipeline iteratively adjusts both the state-transition model and the property set until the model checker confirms that every specification is satisfied. Its output is a final, machine-veriffed NuSMV ffll, thereby closing the loop from informal SOP text to formally validated code. During each refinement cycle we expose the complete code-revision history to the reasoning LLM, enabling it to explore alternative bounds, variable domains and transition guards when repairing syntax or localisation faults. Once these structural issues are resolved, the verifier performs a semantic pass; any SOP requirement remains unmet, the agent replans and the debugging loop repeats until full compliance is achieved.
5

---

Table LLM-Judge evaluation results across five benchmark systems. Each cell shows metric or compliance score, with models grouped by task. Green highlights indicate the top three performers; red marks the bottom two.
represents that the smv artifact failed to execute after debugging.
Structural Alignment
Property Fidelity
Semantic
Code
Code Compliance
Exccution Compliance
Final
Model
Fidelity
Bonus
Compliance Score
BRP Protocol
SpecMAS
5.66
6,84
5.50
0.38
0.55 0.02
0.14
0.76 : 0.08
Claude 25
6.66
8.16
6.84
0.1
0.60 0.08
0.38 1 0.04
0.46 0.05
DeepSeek 26
5.00
5.16
5.34
0.2
0.45 + 0.01
0.5 0.14
0.48 0.08
Gemini 27
7.34
8.84
8.17
0.52
0.75 + 0.04
0.0* +0
0.30 0.01
Qwen 24
6.67
8.00
7.17
-0.14
0.55 + 0.04
0.16 + 0.04
0.32 0.04
Shuttle Autopilot Guidance System
SpecMAS
5.17
0.19
0.45
0.97
0.76 = 0.01
Claude
5.66
6,50
0.25
0.42 0.1
DeepSeek
4.33
0.03
0.07
0.45
0.42 0.07
Gemini
5.66
-0.23
0.04
0.6
0.51 = 0.01
Qwen
5.16
5.16
5.33
0.20
0.04
0.04 0.05
0,20 = 0.04
Mutual Exclusion
SpecMAS
8.5
7.84
7.00
0.19
0.66 + 0.09
0.85 + 0.07
0.77 = 0.08
Claude
9.66
9.5
9.34
0.02
0.76 +: 0.13
0.95 + 0.07
0.88 : 0.09
DeepSeek
8.5
9.16
7.16
0.03
0.66 + 0.13
1.0
0.86 = 0.05
Gemini
9.84
6.5
0.38
0.73 + 0.08
0.85 + 0.07
0.80 - 0.08
Qwen
9.66
10.0
9.5
0.06
0.79 + 0.06
0.1+0
0.38 0.02
Robot Controller
SpecMAS
4.50
3.50
0.28
0.38 0.06
0.90 0.07
0.69 0.07
Claude
6.83
8.34
8.0
0.73
0.76 0.04
0.0
0.30 0.02
DeepSeek
5.16
6.16
5.50
-0.06
0.44 144:00 0.04
0.64 0.06
0.56 0.02
Gemini
8.84
9.34
8.34
0.22
0.75 0.03
0
0.30 0.01
Qwen
6.66
7.17
5.66
0.34
0.58 0.05
0.0* =
0.24 0.02
GigaMax Cache Coherence Protocol
SpecMAS
5.67
4.67
0.46
0.50 0.04
0.84 + 0.06
0.70 + 0.05
Claude
6.5
8,84
6.84
0.27
0.65 + 0.01
0.06 + 0.04
0.29 = 0.01
DeepSeek
6.16
7.16
6,50
0.14
0.56 + 0.01
0.66 0.05
0.62 = 0.02
Gemini
9.34
0.40
0.76 0.01
0.0* 0
0.30 0.01
Qwen
7.16
6.84
-0.08
0.53 0.04
0.61 + 0.01
0.57 0.01
Experimental Setup
We report results on MiniSpeeBench, curated suite of 10 Standard Seeerr--ppraatnn-Preeeee (SOP) documents paired with the reference expert NuSMV model files with CTL/LTL specifiaaiios.. All expert written smv files were taken from the canonical NuSMV example suite distributed with version 2 and later, covering broad spectrum of industrial design motifs. Because the original distribution provides code but no documentation, we automatically synthesised a natural-language SOP for every NuSMV model using customised variant of SYNTHIA [23], supplying the ground- truth smv files as the sole input. SpecMAS queries the SOP documents and the available knowledge base (consisting of documents on formal verification; more information in supplementary material) during agent execution through a retrieval-augmentte generation framework.
Results are averaged over two independent LLM-as-a-Judee evaluation runs. Full results on the MiniSpecBBnch dataset will be included in the supplementary material. The SpecMAS framework uses 8- b-bit-quantised Qwen3-322 model [24] as its backbone reasoning LLM. All experiments are conducted on a workstation equipped with an AMD Ryzen Threadripper PRO 7955WX, 256GB RAM and two NVIDIA RTX A6000 GPUs.
5 Evaluation
evaluate SpecMAS against baseline LLM models using an LLM-as-a-Judge framework for evaluation. Fach generated smv is assessed across three Code Quality metrics- Structural Alignment, Property Fidelity, Semantic Fidelity, along with Bonus metric Code Bonus, and Compliance Scores.

---

Structural alignment captures how faithfully the agent reproduces the topology of the expert model and consists of the following components: (i) role coverage of critical variables, (ii) accuracy of transition logic, and (iii) consistency of the chosen module/define decomposition.
Property fidelity measures the logical equivalence and syntactic similarity between the generated properties and the expert-authored reference properties. It quantifies the quality of the generated CTL/ LTL suite and comprises of: (i) coverage of the SOP- or expert-specified requirements, (ii) logical equivalence to expert formulas, and (iii) syntactic operator correctness. Semantic Fidelity evaluates behavioural soundness: (i) behaviour match under the execution semantics, (ii) treatment of edge cases such as recovery modes or fairness constraints, and (iii) clarity of identifier naming, Property and Semantic fidelity metrics are essential as generated properties can be logically sound and semantically well-formen yet still lead to counterexample traces during model checking due to mismatches in assumptions, missing state conditions, or incorrect variable scoping.
Compliance Scores are mixtures of penalty and reward values that are used to measure the Model's adherence to the input SOP. (i) Code Compliance measures the model's overall coverage of input SOP requirement to NuSMV syntax and module definitions, (ii) Execution Compliance denotes the Model's functional coverage of input SOP in terms of property specifications and state variables and the ability to produce executable code without the presence of counter-example traces. The Bonus Metric evaluates a model's 's ability to generate a NuSMV model that suraasses expert-written wwitten files in quality by exploring additional edge cases, tightening specification bounds, and improving structural modularity beyond the reference implementation. Code Quality metrics are reported on a scale of 10, the Bonus and Compliance scores are in range 0.5, 1] and [0, 1] respectively.
Table presents a detailed evaluation of five systems from Mini SpecBench- Mutual Exclusion for two processes, BRP Message Protocol, Shuttle Autopilot Guidance System, Real-time robot controller, GigaMax Cache Coherence Algorithm. Each system was assessed across total of 17 metrics, which were aggregated into higher-level categories for analysis as described above (implementation details are provided in supplementary material). The Final Compliance Scores are then calculated as the weighted average of the Code Compliance (40%) and Execution Compliance (60%) scores.
The evaluation results highlight significant variations in performance across all models and metries, reflecting the diverse strengths and limitations of each system in the task of generating executable and semantically aligned NuSMV code from SOP documents. Among all models tested, SpecMAS, Claude, and DeepSeek consistently perform better overall, particularly in terms of structural and semantic fidelity. Claude (3.7-Sonnet) performs competitively, particularly in structural alignment and property fidelity, closely trailing SpecMAS on several benchmarks. Both Claude and SpecMAS achieve high Semantic fidelity score, revealing the better instruction following and CoT-based exploration capabilities of these methods. However, Claude's performance drops significantly on execution-senssttvve tasks, as seen in its failure execute the Robot Controller model.
maintains balanced, moderate performance across metrics, ranking third overall, but occasionally struggles with semantic precision in complex safety-critical systems. Gemini (Flash-2.5), despite scoring well on some logical and semantic aspects, suffers from poor execution reliability and fails generate executable models in three out of five tasks. This reflects structural inconsistencies and weaker domain alignment. Surprisingly, Qwen (3.0-Chat-235B8 despite having a much larger parameter count than SpecMAS's Qwen3-32B Sbit model, performs poorly across most tasks particularly in execution. This suggests that SpecMAS's ' advantage does not come from model size or raw reasoning power alone. Instead, its strength lies in the integration of model and specification synthesis with an iterative code debugging pipeline.
DeepSeek DDstiill-llma-
SpecMAS demonstrates the most stable and robust performance across the five benchmark systems, achieving the highest Final Compliance Score for four out of five SOPs evaluated in Table 2 It combines strong formal reasoning, structured synthesis, and execution reliability in single unified framework. It further maintains a strong balance across all evaluation axes: structural alignment, property fidelity, semantic fidelity, and execution correctness. This indicates its superior ability to generalise system behaviours from SOPs into valid formal models. Notably, SpecMAS excels in Execution Compliance, outperforming all other models on this critical dimension.
7

---

Table 3: Comparison of lowest Debug-Stey models vs. highest Final Compliance score models.
SOP
Min Debug-Stepp
Max Compl-Comp Score
A Debug Steps
A Score
BRP Protocol
DeepSeek
SpeeMAS 0.76
+5
+0.28
Shuttle Autopilot
DeepSeek
SpecMAS 0.76
+5
+0.34
Mutual Exclusion
Claude
SpecMAS 0.77
+6
-0.11
Robot Controller
Claude
SpecMAS 0.69
+4
+0.39
GigaMax Cache
DeepSeek
SpecMAS
0.7
+0.08
Oursarbinn Debuggin Dranl denes Medel Gonereted SMeflis
(a) Comparison of debugging/error correction steps required to execute generated smv files.
(b) Comparison of compliance scores for smv files of different SOP system domains in MiniSpecBench.
Figure 2: Evaluation of generation performance across debugging effort and compliance quality.
5.1 Qualitative Analysis of Code Generation and Execution Compliance
For all models except SpecMAS, we measure the number of manual debug steps-defined as the minimal edits required to produce syntax-error-free file. For SpecMAS, we instead track the number of iterations performed by our Debugger Agent, which first resolves syntax errors and then iteratively refines counterexamples until model-checked artifact produced. Figure 2a compares the number of manual debug steps and agent-led repair steps across ten benchmark SOPs. Intuitively, fewer debug steps suggest that an LLM's initial draft is closer to a "compilc-and-vent"
SMV artifact.
However, as shown in Tables 2 Jad 3 once all files are repaired, SpecMAS consistently outperforms all baselines on key metrics such as Structural Alignment, Property Fidelity, and Compliance Scores. This highlights a critical insight: low debug step counts do not necessarily translate into high-quality or high- high-compliance smv files. plausible explanation is that baseline models may produce files that are syntactically valid with minimal edits (or none at all), but structurally incomplete semantically shallow. For instance, DeepSeek requires zero syntax fixes but achieves very low Final Compliance Scores. This suggests that, while its code is "runnable", it often omits critical state variables, transition logic, or property specifications. In contrast, SpecMAS generates drafts that are more detailed and semantically rich-capturing edge cases, nuanced transitions, and full property coverage-which while increasing the likelihood of syntax errors. But this results in much higher semantic fidelity once agentic debugging is applied shown in Figure 26
The tendency baseline LLMs to produce error-prone sMV code is likely linked NuSMV being language, where teken-level exposure during pretraining is minimal. low-resource, hallucination rates, a consistent pattern observed especially in Gemini and Qwen. This leads to higher These issues reinforce the value of providing LLMs with tools and domain-specific context during generation. Our evaluation strongly supports this hypothesis: tool-augmented, context-aware models (like SpecMAS) produce higher-quality artifacts, even if they initially require more debugging effort.

---

Compliance
Dasparsk
Domiri
Dlean
Moder hap buali lpp buck Me Chacking
Ang Spec- Quality
Compl
(a) Ablation study showing impact removing core agent pipelines on final compliance score across selected MiniSpecBench SOPs.
(b) Case study comparing average specification quality (left axis) and execution compliance (right axis) across models for the BRP Protocol SOP.
Figure 3: (a) Contribution of individual agents in SpecMAS to overall model-checking performance.
(b) Analysis of the trade-off between Specification quality (SPEC) and Execution Compliance.
5.2 Ablation Studies for Evaluation of Agent Contributions
The ablation study results shown in BagureB3levallate the incremental contribution of key components within the SpecMAS pipeline, specifically the impact of: (i) The baseline Qwen3 32B 8-bit LLM without planning or verification model, (ii) Model and specifications synthesis alone (iii) the full pipeline including symbolic model checking and debugging-on the Final Compliance score across five benchmark SOPs from Table Each axes is decomposed into two stacked segments representing the weighted contributions of Code Quality and Execution Compliance to the final score.
The ablation results confirm that the key performance gains of SpecMAS are not solely from LLM-based synthesis, but from its integrated verification and debugging loop. While high-quality initial generation important, reliable execution, particularly formal verification tasks, requires post-hoc error correction and planning. This is feature that the full SpecMAS pipeline provides. Synthesis-only pipeline improves code compliance over baseline Qwen model and often fails to produce executable models. For instance, in the Robotics Controller and GigaMax Cache benchmarks, execution performance without debugging counterexample traces remains low.
We observe drop in performance for the Mutual Exclusion SOP when using only the model and specification synthesis pipeline. The intermediate artefact generated at this stage was not executable due to syntax errors and missed explicit state transition condition. Additionally, the property exploration plan introduced a novel property related to turn alternation which was not explicitly required by the SOP. Once the agentic debugging loop activated, it successfully identified and corrected both the structural and property-lever issues.
5.3 Case Study: Evaluating the Impact of Proposed Agents
We observe that although SpecMAS occasionally scores lower than baseline LLMs like Claude and Gemini structural alignment, property fidelity, and semantic fidelity, it still achieves the highest Final Compliance scores. This raises a question about how lower Code Compliance artifacts can outperform more aligned model files in Execution Compliance. We attribute this to two main factors: (1) the execution-centric design of SpecMAS and (2) the brittleness of one-shot generation in baseline models. To illustrate this, we examine the BRP protocol SOP from MiniSpecBennh.
Figure 3b highlights this paradox. plots Exccution Compliance against Average Specification (SPEC) quality for BRP Protocol SOP, calculated the mean of structural alignment, property fidelity, and semantic fidelity. Although Qwen achieves the highest mean SPEC quality score, it fails almost completely in Execution Compliance similar trend can is observed for Gemini well. In contrast, SpecMAS and Claude have more modest average SPEC quality scores, but maintain a high Execution Compliance.
This discrepancy reveals critical flaw one-shot generation approaches. While their outputs may appear structurally or logically correct, they lack post-generation verification, counterexample-guicee -uidee refinement, and $OP-grounded planning- a result, even minor syntax or semantic issues that undetectable by surface-level scoring can lead to failure during NuSMV execution. In contrast,

---

SpecMAS deliberately trades alignment and fidelity scores to incorporate multi- agent planning and automated debugging pipelines that corrects errors before finalizing the model file. This result in lower Code Compliance score, but a substantially higher Execution Compliance- an outcome that is far more valuable for formal verification tasks.
Conclusion
In this work, we introduced SpecMAS, multi-agent framework for generating formally verified sys- tems from natural language SOPs using model checking. Through evaluations on the MiniSpecBench suite, SpecMAS consistently outperformed state-of-the-an L.MMs across key metrics. Our results highlight the value of an execution-centréc multi-agent approach over one-shot code generation. By combining planning, retrieval, and automated debugging, SpecMAS improves the reliability of generated NuSMV models. This work marks step forward in applying agentic LLMs to system synthesis and verification, paving the way for more robust LLM based formal verification agents.
7 Limitations and Future Directions
While SpecMAS demonstrates strong potential for formal self- verification of agentic systems, some limitations remain that highlight valuable opportunities for future research and refinement.
First, handling underspecified or inconsistent SOPs inherently challenging due the variability and ambiguity of real-world documentation. SpecMAS already mitigates this through aassoing-cappbble LLMs, hierarchical planning, and SCMRAG 22 based retrieval to infer missing information and align transitions with the logical intent of the SOP. However, extreme ambiguity may still require human-in -iat--iiittttoooooo assistance. Integrating guided expert feedback into the verification loop is an extension that would enhance semantic fidelity and interpretability without compromising automation.
Second, while the system's property extraction and symbolic relevance checks substantially reduce vacuous or trivial properties, there remains limited risk that certain verified properties may not fully capture the intended operational semantics. The built-in entailment classification and counterexample- based debugging already provide interpretability and grounding, but future versions can incorporate richer semantic reasoning and coverage metrics strengthen this safeguard further.
Third, SpecMAS currently relies on NuSMV for symbolic model checking, which restricts full generalization to hybrid probabilistic systems. Nonetheless, avoidance and shuttle autopilot controller tasks show that the framework can model continuous behaviors through discrete abstractions. Future expansions will integrate complementary verification backends such as SPIN, extending the approach to hybrid and stochastic systems.
results on the traffic collision
Finally, scalability is an ongoing consideration. Symbolic model checking can encounter state- space explosion in high-complexity systems, occasionally increasing reasoning time and debugging iterations. Current results show strong convergence, with an average of only 18 additional steps on the most complex tasks. Future work will explore component- based and modular verification, allowing larger systems be decomposed and verified more efficiently. Also, the current implementation of SpecMAS focuses on generated SOPs rather than human- numan-authored authored documents. This choice was made because existing NuSMV model files lacked corresponding natural- natural-language specifications, making aligned SOP-model pairs unavailable. SYNTHIA was designed to generate semantically faithful yet syntactically diverse SOPs from numan-authored code artifacts. We plan incorporate human-written SOPs future work to assess robustness under natural linguistic variability.
In summary, these limitations represent growth avenues rather than shortcomings, each pointing toward richer semantic understanding, broader generalizability, and improved scalability. Addressing them will further strengthen SpecMAS reliable, interpretable, and extensible framework for formal self- verfficciii of LLM-generated system models.
Acknowledgments and Disclosure of Funding
This research was funded through the MITACS Accelerate Program (Grant IT40058) in partnership with the International Center for Applied Systems Science for Sustainable Development(CAASSS)) Cambridge, Ontario.
10

---

References
[1] Gianpiero Cabodi, Sergio Nocco, and Stefano Quer. Strengthening model checking techniques with inductive invariants. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 28(1):154-18) 158, 2009. doi: 10. 10.1009/CDD2200 2009000..0917.
[2] Dirk Beyer, Matthias Dangl, and Philipp Wendler. Boosting k-induction with continuously- refined invariants. In Daniel Kroening and Corina S. Päsăreanu, editors, Computer Aided Verification, pages 622-640, Cham, 2015. Springer International Publishing. ISBN 978-3-319- 21690-4.
[3] Monika Singh, Ashok Kumar, and Ruhi Saxena. Why formal methods are considered for safety critical systems? Journal of Software Engineering and Applications, 8:531-538, 10 2015. doi: 10.4 10.4236/jsca.211 2015,8 2015.810050
[4] Yue Wang and Sai Chung. Artificial intelligence in safety-critical systems: a systematic review. Industrial Management Data Systems, ahcad-of-print, 12 2021. doi: 10.1108/ IMDS-07-2021-0419.
[5] Xiaoyin Wang and Dakai Zhu. Validating Ilm-gennrated programs with metamorphic prompt testing. 2024. URL https://aaxx: http://ww...g//////////0//// 06844
[6] Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, and Marco Roveri. Nusmv: A new symbolic model verifier. In International conference on computer aided verification, pages 495 499. Springer, 1999.
[7] Yinling Liu and Jean-Michel Bruel. Modeling and verification of natural language requirements based on states and modes. Form. Asp. Comput., 36(2), June 2024. ISSN 0934-5043, doi: 10.1145/3640822. URL http::://oi..
1145/3640822
[8] Hanmeng Liu, Zhizhang Fu, Mengru Ding, Ruoxi Ning, Chaoli Zhang, Xiaozhang Liu, and Yue Zhang. Logical reasoning in large language models: A survey. 2025. URL https
7/arxiv. org/ arrg/bbs/5022. 09100
[9] Sören Preibusch and Florian Kammüller. Checking the twin elevator system by translating object-z to smv. In Stefan Leue and Pedro Merino, editors, Formal Methods for Industrial Critical Systems, pages 38-55, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 08883-540-77707-4
[10] Qian Zhongsheng, Li Xin, and Wang Xiaojin. Modeling distributed real-time elevator system by three model checkers. International Journal of Online and Biomedical En- gineering (iJOE), 14(04):pp. 94-110. Apr. 2018. doi: 14:4/ URL
https://online- journals.......... org/indez.
[11] Mengyan Zhao, Ran Tao, Yanhong Huang, Jianqi Shi. Shengchao Qin, and Yang Yang. N12ctl: Automatic generation of formal requirements specifications via large language models. In Kazuhiro Ogata, Dominique Mery, Meng Sun, and Shaoying Liu. editors, Formal Methods and Software Engineering, pages 1-17, Singapore, 2024. Springer Nature Singapore. ISBN 778-981-96-06177
[12] Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu. Proper- tygpt: LIm-driven formal verification of smart contracts through retrievallaugmeeted prop- erty generation. In Proceedings 2025 Network and Distributed System Security Sympo- sium, NDSS 2025, Internet Society, 2025. doi: 10.14722/mdss.0255.. //dx.doi. orgi 10. 14722/ndss..s 2025.0222222222 241357
URL http
[13] Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing Bhing-Chi Cheung, and Cong Tian. Enchanting program specification synthesis by large language models using static analysis and program verification. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification, pages 302-328, Cham, 2024. Springer Nature Switzerland. ISBN 978-3-031-65630-

---

[14] Lezhi Ma, Shangqing Liu, Li, Xiaofei Xie, and Lei Bu. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE), pages 666-666, Los Alamitos, CA, USA, May 2025. IEEE Computer Society. doi: 10.1 10.1109//CSS555334.... 2025.0025.000 29. URL https://doi. wewccompteerooclttyyooooo org/ 1109/ 1.01999SSE5534777 2025. .01299
[15] Cormac Flanagan and K. Rustan M. Leino. Houdini, an annotation assistant for esc/java. In Proceedings of the International Symposium of Formal Methods Europe Formal Methods for Increasing Software Productivity, FME '01, page 500-517, Berlin, Heidelberg, 2001. Springer- Verlag. ISBN 3540417915.
[16] Michael D. Ernst, H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Science of Computer Programming, 69(1):35-45, 2007. ISSN 0167-6423. doi: https://doi.org/ (t11ff/scico.200.000..11 URL https: //www sci sciencedirect. com/ sttssscincccceeeeeeeee/ acience/article./ articee/ p11/5016764230700161.1 Special issue on Experimental Software and Toolkits.
[17] Guangyuan Wu, Weining Cao, Yuan Yao, Hengfeng Wei, Taolue Chen, and Xiaoxing Ma. Llm meets bounded model checking: Neuro-symbolic loop invariant inference. In Pro- ceedings of the 39th IEEF/ACM International Conference on Automated Software Engi- neering. ASE '24, page 406-417, New York, NY, USA, 2024. Association for Comput- doi: 10.1145/36916203669999
ing Machinery. ISBN 97984007122 12487.
URL https
//doi. 10. 1145 116166662333666
[18] Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19:7-34, 01 2001. doi: 10.1023/A: 101 1011276507260.
[19] Muhammad A. A. Pirzada, Giles Reger, Ahmed Bhayat, and Lucas C. Cordeiro. Lim- generated invariants for bounded model checking without loop unrolling. In Proceedings of the 39th JEEE/ACM International Conference on Automated Software Engineering, ASE '24. page 1405,1407, New York, NY, USA, 2024. Association for Computing Machinery. doi: 10. 00.1145/369162.000 32..369551.. URL, httph:t/t///oo org/10........ 1145/
ISBN 9798400712487.
3691620. 3691620.3695512 3695512
[20] Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In Natasha Shary- gina and Helmut Veith, editors, Computer Aided Verification. pages 1-35, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. ISBN 978-3-642-39799--
[21] Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. The seahorn verification framework. In Daniel Kroening and Corina S. Päsäreanu, editors, Computer Aided Verification, pages 343-361, Cham, 2015, Springer International Publishing. ISBN 978-3-319-21690-4,
[22] Bharti Chimdyalwar, Priyanka Darke, Avriti Chauhan, Punit Shah, Shrawan Kumar, and R. Venkatesh. Veriabs: Verification by abstraction (competition contribution). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2017. URL https://api. semanticscholas http::://pp..smmatiicccoooo
Drg/Corpus.ID:::2 2122619
[23]
Anonymous. SYNTHIA: A multi-agent GAN- fusion for statistically guided synthetic data generation. 2025.
under review.
[24]
An Yang et al. Qwen2.5 technical report. arXiv preprint arXiv:2412.155115 2024.
[25]
Anthropic. The claude 3 model family: Opus, sonnet, haiku. Brg.0//abbbbaaaaaooooaoob6/33600 pdf Published March 4, 2024; accessed May 16, 2025.
March 2024. URL
https: /ttps://www--a cdn. anthropic https://wwwwcch.aatrree
Model_Card__Caudee
[26] DeepSeek-AI, Daya Guo, et al. Deepseek-rl: Incentivizing reasoning capability in llms reinforcement learning. 2025. doi: http://dl.ooyylll.855saavvv.....
URL
btops://arrhhs .og//og///...................... http/dff/50// /200 12948
12

---

[27] Gemini Team. Gemini: A family of highly capable multimodal models. 2024. URL https
7/arxiv. htt/abb//312... 11805
[28]
Jiawei Gu, Xuhui Jiang, Zhichao Shi, Hexiang Tan, Xuehao Zhai, Chengjin Xu, Wei Li, Yinghan Shen, Shengjie Ma, Honghao Liu, Saizhuo Wang, Kun Zhang, Yuanzhuo Wang, Wen Gao, Lionel Ni, and Jian Guo. A survey on llm-as-a-judge. 2025. /tttp:s::///r orw.bbs../b///./. /bs
[29] Rishabh Agrawal, Murtaza Asrani, Hadi Youssef, and Apurva Narayan. Semrag: Self-corrective multihop retrieval augmented generation system for Ilm agents. In Proceedings of the 24th International Conference on Aulonomous Agents and Multiagent Systems, AAMAS '25, page 50-58, Richland, SC, 2025. International Foundation for Autonomous Agents and Multiagent Systems. ISBN 9798400714269.
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: Sections and 5.3 cover the major claims we've made. Section 5.2 provides an explanation for our claims.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
It is fine to include aspirational goals as motivation long is clear that these goals are not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations of the work performed by the authors? Answer: [No]
Justification: We have briefly discussed certain limitations in the paper; full, detailed discussion will provided in the supplementary material.
Guidelines:
The answer NA means that the paper has no limitation, while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limitations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (c.g.. independence assumptions, noiseless settings, model cell-speciiiiatinn asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g. if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-tex, system might not be used reliably to provide closed captions for online lectures because it fails handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and faimesss.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community, Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
14

---

Answer: [NA]
Justification:
We talk about our experimental results and their analysis on a benchmark
dataset.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but they appear in the supplemental material, the authors encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification: We have discussed in detail the reproducibility of our main experimental results in Sections 4 and 5.
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reprodueibility may be tricky in some cases, in which authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
5. Open access to data and code
15

---

reproducible, they Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [No]
Justification: All the data and code files will be provided as part of the supplementary material.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips.co cc/
for more details.
While we encourage the release of code and data, we understand that this might be possible, so "No" is an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https
/ https//ccppblccc/uuuddeeeoo Coaee//ddeeeebmmmcia ssi onPolicy) for more details.
The authors should provide instructions data access and preparation, including how to access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. only subset of experiments should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: Section talks about the experimental setup in detail.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to a level of detail that is necessary appreciate the results and make sense of them.
The full details can provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [NA]
Justification: We perform quantitative and qualitative analysis for our results as explained in Section 5.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
16

---

The method for calculating the error bars should be explained (closed form formula, call a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful figures symmetric error bars that would yield results that are out of range (e.g. negative rates).
show in tables or
If error bars are reported in tables or plots, The authors should explain the text how they were calculated and reference the corresponding figures tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We provide detailed information about our experimental setup Section 4.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs as well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't 't make it into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification: Our work does conform to NeurIPS Code of Ethics.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is special consid- cration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [No]
Justification: Our work focuses primarily on foundational research and does not directly address immediate societal impacts.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
17

---

Examples of negative societal impacts include potential malicious unintended uses (e.g., disinformation, generating fake profiles, surveillance), faireess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper deseribe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: We believe the nature of our work presents minimal risk of misuse. Nonetheless, we remain mindful of responsible research practices and are open incorporating safeguards should future developments introduce any potential concerns.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g.. code, data, models), used in the paper. properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: We have ensured that all original creators of the files and LLMs used in our experiments are appropriately credited. Additionally, we have adhered to the relevant licenses and terms of use associated with these assets.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL
The name of the license (e.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
18

---

If assets are released, the license, copyright information, and terms of use in the thcode. has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
package should be provided. For popular datasets, paperswi
latasets.papersstt
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification: We introduce assets in Section 4 of the paper, including the benchmark suite and evaluation framework. Additional documentation and usage instructions will be provided in the supplementary materials to ensure reproducibility and ease of use.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset is used.
At submission time, remember anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: Our work doesn't 't involve the use of crowdsoureing nor research on human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: Our work doesn't 'tt involve crowdsourcing nor research done on human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
19

---

Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if' applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Question:
Answer: [Yes]
We describe the usage of LLMs as a central component of our core method- ology. Specifically, our framework leverages LLMs for the generation, refinement, and evaluation.
Justification:
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our LLM policy for what should or should not be described.
http://upppssccooeeeeeeeeeeeeeee /
20


Reviews:
[{"review_id": "kQ25RvhJpg", "reviewer": "Reviewer_YKJx", "summary": "This paper presents a framework for synthesizing and verifying programs from natural language descriptions (Standard Operating Procedure). The framework represents the generated system as a finite-state transition system along with CTL/LTL specifications. The framework integrates LLMs and verification tools. In particular, LLMs are used to parse SOP, generate specifications, and make corrections. The paper demonstrates that SpecMAS outperforms program synthesis approaches that directly invoke a language model across a number of benchmarks over several metrics.", "questions": "- How is the number of minimal edits computed? Is it provably the minimal number of edits, or is it the empirical number of edits made by some human?\n- Is SpecMAS fully automated?\n- I imagine that the LLM was trained less on NuSMV text than other more common languages (e.g., C, Python). Have the authors encountered cases where the LLM has trouble generating syntactically correct models?", "limitations": "The checklist suggests that there will be a discussion of limitations in the supplementary materials, but I did not find such discussion there.", "rating": 3, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 1, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths\n- This paper presents a framework that combines the strengths of LLMs and formal verification tools to generate programs that provably satisfy the extracted specifications. The framework is novel as far as I can tell.\n- Leveraging existing framework like NuSMV seems like a good design choice.\n\nWeaknesses:\n- Ultimately, any approach that goes from natural language to formal language lacks formal guarantees on the correctness of the generated program. This work is no exception. This makes the use of formal verification techniques (which are expensive processes) less well-motivated.\n- In order to improve the trust in the generated program, it seems the correctness of the synthesized specifications is important, otherwise the verification would not be meaningful. The paper lacks a rigorous analysis on the correctness of the generated specifications. What comes close to it is the measurement of Property Fidelity. However, SpecMAS is not competitive on this measure compared to baseline methods.\n- The main methodology section is only a little over 2 pages, and stays at a very high-level. This makes it really difficult to fully grasp the workflow. I understand there is a page limit, but in its current form, the methodology reads quite thin and abstract. Walking through those steps with a working example would greatly improve the readability of the paper.\n- The benchmarks are generated from existing NuSMV examples via SYNTHIA (not real human-written SOPs). This may lead to unrealistically clean natural language inputs. It would be interesting to test on existing natural language benchmarks or SOPs written by humans.", "was_revised": false, "final_justification": "", "rebuttal": "# Rebuttal – Reviewer YKJx\n\nWe thank the reviewer for their thorough reading and insightful suggestions. Their feedback already strengthens SpecMAS. Below are each point addressed in turn, with references to the sections in the paper or supplementary section wherever possible.\n\n---\n\n## 1) Formal Guarantees and Specification Correctness\n\nThe core contribution of SpecMAS is to address the issue of verifying LLM generated system outputs through a closed-loop verification process. While it is true that no natural language-to-code system can offer a priori guarantees on correctness,  \nSpecMAS ensures correctness of extracted properties through iterative model checking.\n\nAs outlined in Section 3.1, SpecMAS avoids the pitfalls of one-shot synthesis by generating NuSMV specification files that are aligned with both explicitly stated and implicitly inferred logical constraints. Crucially, when a specification fails during model checking, SpecMAS automatically interprets the counterexample traces returned by NuSMV and uses them to refine the system model and specifications without requiring human intervention. This loop continues until all counterexamples are eliminated and the model satisfies all properties. Thus, even when the initial specifications are noisy or incomplete, the Model Generator, Coding, and Debugging Agents work collaboratively to correct structural and logical errors in an automated, iterative manner.\n\nThe final output received from the SpecMAS system is machine-verified. This makes the use of formal verification both justified and essential. It elevates the reliability of a stochastic generative process into a provably correct artifact. This is also reflected in our evaluation where SpecMAS consistently produces executable and verified NuSMV model files. In contrast, larger LLMs often fail to generate functionally correct artifacts even after multiple debugging attempts.\n\n---\n\n## 2) Trust in Generated Specifications\n\nWe agree that the correctness of the synthesized specifications is central to meaningful verification. Property Fidelity (defined in Section 5) is our primary metric for evaluating this aspect. While SpecMAS may not always achieve the highest Property Fidelity score across all systems, SpecMAS achieves the best Final Compliance Scores on 4 out of 5 benchmarks. This metric includes Execution Compliance which is a more rigorous indicator of whether the generated specifications are actually valid and verified, and not just syntactically plausible.\n\nOur case study (Section 5.4, Figure 3b) demonstrates this key insight: high Property Fidelity does not necessarily translate into successful model execution. Baseline LLMs that appear to generate structurally correct properties often fail at execution time due to missing transitions, unverifiable invariants, or incomplete property sets. SpecMAS trades some property fidelity for more robust executability which is valuable for safety-critical applications requiring provable correctness.\n\n---\n\n## 3) Methodology Details\n\nThank you for this valuable suggestion. Due to page limits, we summarized the methodology and chose to prioritize our core contributions and evaluation in the main paper. We will include a Step-by-Step walkthrough of SpecMAS using a concrete example from MiniSpecBench along with intermediate outputs such as extracted states, transitions, and properties, as well as debugging traces and final verified code in the supplementary section.\n\n---\n\n## 4) Benchmark Authenticity\n\nWe appreciate this concern and acknowledge that SpecMAS does not use human written SOPs in its evaluation. We opted to use SYNTHIA-generated SOPs because the ground truth NuSMV model files lacked natural language documentation, making aligned SOP and NuSMV model file pairs unavailable. However, SYNTHIA was explicitly designed to generate semantically faithful but syntactically diverse SOPs in natural language from human authored code artifacts. These SOPs paraphrase the system’s functional requirements. We manually checked all generated SOPs to make sure it did not contain any explicit mention of NuSMV style temporal properties or transition logic to avoid trivializing the task. All generated SOPs are available in the supplementary material. However, we acknowledge this limitation and will explore Human-written SOPs in future work.\n\n---\n\n## Technical Clarifications\n\n- **Minimal edits (Debugging Steps):** For SpecMAS we recorded the number of steps taken by the debugger agent until a successful execution is reached. For baseline LLMs, it was computed manually by iteratively prompting each LLM model with the corresponding error trace after every execution of its updated NuSMV code. This is done up to a maximum of 60 debug steps.\n\n- SpecMAS is fully automated once initialized and requires no human intervention.\n\n- LLMs do struggle with NuSMV syntax. We encountered cases where LLMs had issues with generating valid NuSMV syntax, inability to follow the set program structure i.e INIT, VAR, ASSIGN etc. Which is precisely why our debugging agent is essential in the architecture of SpecMAS.\n\nWe will add a brief limitations section addressing these concerns in supplementary material and expand it with more specifics and edge cases."}, {"review_id": "MGPTBb1NIr", "reviewer": "Reviewer_vGPi", "summary": "SpecMAS presents a multi-agent framework that translates natural language Standard Operating Procedures (SOPs) into formally verified NuSMV models. It features two tightly coupled pipelines: a synthesis agent that generates models and specifications, and a debugging agent that uses model checking feedback to iteratively refine the output until all properties are satisfied. Evaluation on the MiniSpecBench dataset shows that SpecMAS outperforms LLM baselines across several compliance and semantic fidelity metrics.", "questions": "How would SpecMAS handle inconsistent or underspecified SOPs in real-world documentation?\n\nCan the approach generalize to hybrid systems (e.g., with continuous dynamics)? Could the authors release MiniSpecBench to foster benchmarking standardization?\n\nAre there plans to extend the framework to support probabilistic or temporal stochastic model checkers? What about the state space explosion problem with nusmv models?\nCan you quantify the performance cost of the multi-agent debugging loop in high-complexity specifications?", "limitations": "No major concerns. The paper explicitly addresses the synthetic SOP generation process, the limitations of NuSMV, and trade-offs in fidelity versus execution.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\nFirst work to propose an agent-based closed-loop pipeline for formal model generation from natural language using NuSMV. Strong architecture, comprehensive experiments, robust benchmarking across multiple domains.\n\nOffers a scalable and generalizable framework that can bridge natural language and formal verification – a key need in system synthesis. The writing is dense but clear, with well-annotated diagrams and detailed evaluations.\n\nWeakness:\nReliance on NuSMV may limit expressivity in modeling probabilistic or timed systems. \n\nSOPs are synthetically generated for some benchmarks, raising concerns about real-world applicability. The debugging loop might struggle with ambiguous or highly underspecified SOPs – not thoroughly evaluated.", "was_revised": true, "final_justification": "I am maintaining my score of 5 (Accept).\n\nThe paper presents a novel, well-executed approach for bridging natural language SOPs and formal verification through an agent-based, closed-loop architecture. It fills a significant gap between NLP and formal methods, and the rebuttal reinforces the contribution's robustness, generality, and future potential.", "rebuttal": "# Rebuttal – Reviewer vGPi\n\nThank you for your positive assessment and recognition of our framework’s contributions. We appreciate your insightful questions about extensions and limitations.\n\n---\n\n### Question: “How would SpecMAS handle inconsistent or underspecified SOPs in real-world documentation?”\n\nThis is a critical point and one of the central challenges SpecMAS is designed to address. In its current form, SpecMAS leverages a reasoning-capable LLM, hierarchical planning, and SCMRAG-based context retrieval to resolve ambiguities present in the SOP. Importantly, the Specification and Model Generator agents are capable of extracting both explicitly stated and implicitly inferred properties and transitions, ensuring alignment with the underlying logical structure of the SOP, even when parts of it are underspecified. That said, we acknowledge that extreme ambiguity may still require external resolution, and in future work, we plan to explore incorporating a human-in-the-loop component to assist in such cases while maintaining interpretability in the model generation process.\n\n---\n\n### Question: “Can the approach generalize to hybrid systems (e.g., with continuous dynamics)?”\n\nWe agree that our current reliance on NuSMV limits the framework to continuous and non-probabilistic systems. We chose NuSMV as it is a mature, industry-standard symbolic model checker, making it an ideal starting point. A natural direction for future work would be to extend the framework to support other verification engines, such as PRISM, TLA+, SPIN etc by creating new toolsets for these agents.\n\nSpecMAS does generalize to systems with continuous dynamics as illustrated by the (Traffic collision avoidance) and (Shuttle autopilot controller) examples in the Benchmark dataset. These systems model the continuous behaviour of traffic or aircraft guidance systems with dynamic variables.\n\n---\n\n### MiniSpecBench Release\n\nWe plan to publicly release the proposed MiniSpecBench dataset, including the SOPs, expert models and evaluation scripts at a later date. These files are provided in the supplementary material of the submission.\n\n---\n\n### State Space Explosion\n\nWe recognize that symbolic model checking can suffer from state space explosion, especially for large systems. For instance, in our experiments with a deadlock detection algorithm containing an extensive number of state variables, SpecMAS required significantly more reasoning time and a higher number of debugging iterations to resolve all counterexample traces. To address this, we plan to explore component-based verification techniques in future work. This would enable SpecMAS to decompose large systems into smaller, independently verifiable modules and improve scalability without compromising correctness.\n\nWe conducted a comparative analysis of examples with the highest Final Compliance Scores relative to the number of debugging steps (see Table 3). However, we have not yet quantified the performance cost of the multi-agent debugging loop for high-complexity specifications, as our current benchmark does not explicitly distinguish SOPs of that category. On average, the debugging agent takes 18 steps more to debug highly complex specifications. We will consider including more detailed analysis of debugging agent in future work."}, {"review_id": "GQ6HAnCVtQ", "reviewer": "Reviewer_5uhY", "summary": "This paper describes the use of LLMs to synthesize finite state models from informal natural language descriptions. These models are amenable to automatic verification using model checking. The approach uses the NuSMV tool for verification with respect to temporal properties, which are also extracted from the documentation. The models are iteratively refined by the LLMs with the help of counterexamples obtained from NuSMV. An evaluation is presented, using several LLMs using 10 mini benchmarks created by the authors.", "questions": "Please provide a detailed description of: prompts, benchmark sizes, properties, and metrics. Adding these details would greatly strengthen the paper.", "limitations": "yes", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Pros:\n\n*    This work is in the same line as verifiable code generation with LLMs but it targets higher-level models that are amenable to formal verification with NuSMV, This seems to be a new, promising target application for LLM generation.\n\n* The approach is well designed: a reasoning agent extracts both explicit and implicit properties from the system description, verification is performed via model checking and another debugging agent analyzes counterexamples and iteratively corrects the model until all properties are satisfied. \n\n*    Results show that the use of model checking produces better results than \"self-verification\" with LLMs.\n\nCons:\n\n*    The line of work is very promising but the paper seems premature; it is written at a very high level with many details missing. It is not clear what prompts were used and also if any few shot examples were used to \"help\" with he process. Was any fine tuning necessary?\n\n*    It is not clear what the size is for each generated model.\n\n*    The paper is also missing a description of the properties that were verified. Were there any properties that would hold vacuously?\n\n*    It is unclear what metrics were used for Table 2. They are described informally without a precise definition.", "was_revised": false, "final_justification": "", "rebuttal": "# Rebuttal – Reviewer 5uhY\n\nWe thank the reviewer for recognising the promising nature of our work and your constructive suggestions for further improvement. We have addressed your questions below.\n\n## Prompts and Few-Shot Examples\n\n- The full prompt templates used by each agent are provided in **Section 5** of the supplementary material, and additional prompts are covered in the `Code` folder of the zip file with the suffix `*_templates.py`. We also provide the entire **MiniSpecBench** dataset in the supplementary zip file. We acknowledge that including specifics on property definitions and evaluation metrics would further strengthen the paper. To address this, we have included the relevant source code in the supplementary material and we will expand it with implementation details in the supplementary section of the final version.\n\n- Our framework does not use few-shot examples in the traditional sense. Instead, it leverages **SCMRAG** to retrieve contextual knowledge from a knowledge base, which includes NuSMV documentation and model checking principles (see **Section 4** of the supplementary material). For instance, when extracting states and dynamic variables, the Model Generator Agent may request background knowledge on Kripke structures, and formal methods for representing system states in the information gathering phase. This enables informed and accurate model synthesis.\n\n## Model Configuration\n\n- We confirm that no model fine-tuning was performed. Our framework utilizes the off-the-shelf **Qwen3 32B** model in reasoning mode, quantized to 8 bits.\n\n## Benchmark Sizes and Metrics\n\n- The average file size for our SOP documents is **32.7 KB**. As for generated NuSMV models, the minimum file size is **3 KB** and the maximum is **8 KB** (BRP protocol), with an average of ~14 **SPEC** properties and a maximum of 20 (priority-queue model), representing realistic complexity for many safety-critical systems.\n\n- We verify standard temporal logic properties generated by the **Specification Generator Agent**. This agent systematically analyzes the input SOP to identify both explicitly stated properties and implicitly required properties related to **safety**, **liveness**, **fairness**, **reachability**, and **temporal ordering** (see `extraction_templates.py` in the supplementary material for prompt details). The resulting candidate properties are then passed to the **Debugging Agent**, which iteratively verifies them using **NuSMV** until all counterexample traces are resolved.\n\n  While some properties may hold trivially if directly requested in the SOP, the agent does not generate vacuous properties. Our **Property Extractor Agent** is explicitly designed to extract semantically meaningful properties that are grounded in the system’s operational logic. Furthermore, since our SOPs are derived from expert-written NuSMV models, the extracted properties retain both semantic relevance and verification significance, ensuring that the verification process remains aligned with the system’s intended behavior.\n\n- We have discussed the metrics in **Section 5** of the paper and provide the source code for evaluating all metrics in the supplementary material. However, we acknowledge the necessity of formal definitions for relevant metrics and will include them in the supplementary section of the final version.\n\n---\n\nWe appreciate your assessment that this work is promising and will incorporate these detailed specifications to strengthen the paper's technical contributions and reproducibility."}, {"review_id": "vxVywXXXIM", "reviewer": "Reviewer_hC91", "summary": "The paper proposes a general methodology for generating exacutable systems from NL specification and uses symbolic model checking, and the NuSMV tool in particular, to validate the systems generated", "questions": "Why are you bringing multiagents into your paper? I understand that this is your general long-term reference application scenario. But, it seems to me, that all you have done is largely independent of this. All the work you have done applies to single FSM, possibly composed from simpler FSMs\n\nYour citation of NuSMV is wrong. If you type NuSMV to scholar you will find appropriate citations starting from the very early paper(s)", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 4, "originality": 4, "strengths_and_weaknesses": "strengths\n- The approach is novel. It is not an incremental evolution of the SoA\n- the work is a concete tentative to generate systems which are highly reliable, by building on the extensive work done in the formal methods community\n\nWeaknesses\n- no major weaknesses", "was_revised": true, "final_justification": "In my opinion, this paper should definitely be accepted. It is a first serious attempt to deal with the problem of how to understand an informal input correctly. It draws on state-of-the-art formal methods techniques, and it applies them in this context. It is a first step in a promising direction which can bring the community a new way of dealing with the general problem of hallucinations and the like.\n\nThe process of going from informal to formal specifications is extensively studied in formal methods. And this is another good reason why this paper should be accepted, as it opens the way to more cross-fertilisation. At the same time, the domain of application is new and much more complex (in terms of ambiguity of the input) with respect to the mainstream work on formal methods. Here, in fact, the input is kept as simple as possible in order to minimise mistakes.\n\nAll in all, this work paves the way for possible cross-fertilisation between two communities which are quite far apart but have a lot to say to each other.", "rebuttal": "# Rebuttal – Reviewer hC91\n\nWe appreciate the reviewer’s observation and the opportunity to clarify the role of the multi-agent design in our framework. While it is true that the final output of **SpecMAS** is a formally verified finite-state model (FSM), the multi-agent architecture is central to how the finite-state model is constructed, verified, debugged and refined from natural language input.\n\n## **SpecMAS** consists of functionally distinct agents, each responsible for a critical stage:\n\n1. Parsing and reasoning over SOPs  \n2. Extracting states and transitions  \n3. Inferring explicit and implicit temporal properties  \n4. Verifying and debugging the model using NuSMV counterexamples  \n\nThese agents coordinate via shared memory and planning, and their outputs are verified and refined in a closed-loop manner. This agent-based decomposition allows **modularity**, **specialization**, and **recursive self-correction**, which are difficult to achieve in a single-agent or monolithic system.\n\nMoreover, the proposed design enables **scalability** and **generalisability**. For instance, in future versions, **SpecMAS** can be specialized to handle hybrid systems, different model checkers, or real-time constraints without modifying the entire architecture. We believe this structured, agent-oriented approach is critical for bridging unstructured natural language specifications with the requirements of formal verification.\n\nWe will revise the citation of NuSMV and include appropriate citations for the relevant earlier papers as well."}]

Author rebuttal:

Meta-review: This paper introduces SpecMAS, a framework that synthesizes and verifies programs from natural language descriptions, specifically Standard Operating Procedures (SOPs). The approach uses Large Language Models (LLMs) to parse SOPs, generate formal specifications (CTL/LTL), and iteratively correct a finite-state transition system model. This model is then verified using formal methods tools. SpecMAS is shown to outperform LLM-only program synthesis baselines across multiple benchmarks and metrics.

This paper makes a strong contribution by introducing a novel framework that effectively bridges natural language processing and formal methods. It combines LLMs and verification tools, like NuSMV, within a closed-loop architecture to generate programs that provably meet formal specifications extracted from text. The approach is well-executed, with comprehensive experiments demonstrating robustness across multiple domains. While the use of synthetic SOPs somewhat limits real-world applicability and certain implementation details are omitted, the work remains impactful, generalizable, and full of future potential.
Decision: Accept (poster)