Formal verification can be a complementary approach to UCD, offering a systematic and repeatable process to address the demands of designing safety and mission-critical interactive systems. However, the practical application of formal verification often encounters barriers to accessibility for non-technical stakeholders. In the case of model checking, although the verification step is fully automated, developing the required specifications and interpreting the verification results requires considerable technical expertise in formal methods. Recent developments in generative Artificial Intelligence (AI) have driven proposals for Large Language Models (LLMs) to be applied throughout various phases of software engineering. This begs the question of whether LLMs might be used to help bridge the gap between formal techniques and tools and stakeholders lacking technical expertise. This paper explores how these questions might be addressed in the context of an ongoing effort aimed at translating model-checking counterexamples into natural language explanations, making them accessible to designers and domain experts.