Incomplete and ambiguous requirements remain a common source of defects in safety-critical software systems. Formal methods provide rigorous correctness guarantees but rely on precise specifications, while Large Language Models (LLMs) enable flexible natural-language processing but lack logical consistency guarantees. Bridging the gap between informal stakeholder intent and formally verifiable specifications remains a key challenge in automated software engineering. This paper presents C-GRiD (Counterexample-Guided Requirements Discovery), a neuro-symbolic framework that integrates model checking into the requirements elicitation process. C-GRiD uses an LLM to synthesize an initial system model and a set of candidate requirements properties, which are then analyzed by a symbolic verifier. Counterexamples generated by the verifier are converted into structured natural-language queries that elicit missing constraints from stakeholders. This enables an iterative refinement loop that progressively reduces specification incompleteness while maintaining logical grounding of generated artifacts. We evaluate C-GRiD on 10 benchmark specifications using a controlled constraint-removal protocol to measure requirement recovery. Under a perfect oracle assumption, the framework achieves a mean constraint recovery recall of 79.2%. To assess robustness under realistic interaction settings, we introduce a simulated noisy stakeholder with a 25% error rate. In this setting, C-GRiD maintains a recall of 70.8%. Results show consistent improvements over one-shot and template-based baselines, demonstrating that counterexample-guided refinement can support the construction of more complete and logically grounded software specifications.

@inproceedings{paperbot12300,
  title = {Neuro-symbolic Requirements Elicitation: Utilizing Formal Verification Counterexamples as Contextual Prompts},
  author = {Okba Tibermacine and Chouki Tibermacine},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3834379}
}