Rebuttal – Reviewer hC91

We 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.

SpecMAS consists of functionally distinct agents, each responsible for a critical stage:

1. Parsing and reasoning over SOPs
2. Extracting states and transitions
3. Inferring explicit and implicit temporal properties
4. Verifying and debugging the model using NuSMV counterexamples

These 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.

Moreover, 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.

We will revise the citation of NuSMV and include appropriate citations for the relevant earlier papers as well.

The answer provided satisfies my request. I confirm my acceptance evaluation.

Rebuttal – Reviewer 5uhY

We thank the reviewer for recognising the promising nature of our work and your constructive suggestions for further improvement. We have addressed your questions below.

Prompts and Few-Shot Examples

• 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.

• 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.

Model Configuration

• 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.

Benchmark Sizes and Metrics

• 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.

• 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.

  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.

• 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.

We appreciate your assessment that this work is promising and will incorporate these detailed specifications to strengthen the paper's technical contributions and reproducibility.

Rebuttal – Reviewer vGPi

Thank you for your positive assessment and recognition of our framework’s contributions. We appreciate your insightful questions about extensions and limitations.

Question: “How would SpecMAS handle inconsistent or underspecified SOPs in real-world documentation?”

This 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.

Question: “Can the approach generalize to hybrid systems (e.g., with continuous dynamics)?”

We 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.

SpecMAS 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.

MiniSpecBench Release

We 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.

State Space Explosion

We 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.

We 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.

Rebuttal – Reviewer YKJx

We 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.

1) Formal Guarantees and Specification Correctness

The 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,
SpecMAS ensures correctness of extracted properties through iterative model checking.

As 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.

The 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.

2) Trust in Generated Specifications

We 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.

Our 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.

3) Methodology Details

Thank 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.

4) Benchmark Authenticity

We 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.

Technical Clarifications

• 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.

• SpecMAS is fully automated once initialized and requires no human intervention.

• 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.

We will add a brief limitations section addressing these concerns in supplementary material and expand it with more specifics and edge cases.

Thank you for your responses. It addresses some of my questions.

I'm still not satisfied with the measurement of specification correctness. The fact that there is a tradeoff between property fidelity and execution compliance is curious. It seems to indicate that property fidelity is not really a rigorous account of whether the generated specifications are actually the correct ones to verify. If it is indeed measuring this, then the message would be that specification synthesis (and verification) is not quite relevant to the quality of the final generated program.