Summary
Ferrari and Spoletini map the bidirectional relationship between LLMs and formal requirements engineering. In one direction, LLMs can generate, translate, and explain formal specifications — lowering the barrier to adoption. In the other direction, formal specifications provide a ground truth against which LLM-generated code can be verified. The paper identifies open challenges: hallucinated specifications, inconsistency detection, and the need for human-in-the-loop validation.
What it means for our work
This paper frames the exact problem space Z Spec and Use Cases occupy. The bidirectional flow — code2model (extract specs from code) and model2code (generate code from specs) — maps directly to Z Spec’s two core commands. The hallucination concern they raise is why we route through fuzz and ProB for type-checking and model-checking rather than trusting LLM-generated specs at face value. The formal tools are the verification layer.