Scope and Motivation

This workshop explores the intersection of formal requirements engineering and artificial intelligence (AI), addressing a central challenge in modern software and AI system development: how to precisely specify requirements for increasingly complex, heterogeneous, and autonomous systems, and how to verify and validate that such systems meet those requirements.

As AI technologies become deeply embedded in safety and mission-critical domains, from autonomous vehicles to medical diagnostics, financial systems to industrial automation and space exploration, the need for rigorous, formal approaches to requirements is becoming increasingly important. At the same time, traditional requirements engineering methods face new challenges when applied to systems with learning-enabled components, unpredictable behaviors, and emergent properties. The opacity of AI models and the semantic gap between high-level requirements and low-level model inputs and internals create significant impediments to verifying and validating that such systems meet their specified requirements.

The workshop welcomes extended abstract contributions on formal specification languages for AI systems, verification and validation techniques, requirements for trustworthy AI, case studies from real-world applications, and novel applications of AI to requirements engineering itself. We aim to foster dialogue between communities that have traditionally worked separately, building bridges toward more reliable, safe, and trustworthy AI systems grounded in rigorous requirements practices. Extended abstracts can summarize and cite results from recent published paper(s) and/or state your perspective.

Topics of Interest

  • How can we formally specify requirements for systems with learning-enabled components?
  • How can formal frameworks capture fairness, safety, robustness and explainability requirements for AI systems?
  • How do we verify that AI systems meet their specified requirements?
  • What role can AI play in automating requirements elicitation, formalization analysis, and validation?
  • How do we bridge high-level requirements and behavior of AI-enabled systems to enable traceability, safety assurance, and certification?

Submission TL;DR

Submission Guidelines

We invite extended abstracts 2-4 pages in length, https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines. All papers should be in English and fall into one of the following categories:

  • New and Emerging Work: Presents novel research in the focus areas of the workshop. Submissions will be evaluated primarily on "novelty".
  • Summary of Recent Results: Presents existing work and highlights its contribution in terms of relevance and impact in the focus areas of the workshop. Submissions will be evaluated primarily on "impact".

Please note that:

  • No Formal Proceedings:We welcome submissions of work that has already been presented or submitted elsewhere. No copyright transfer is required; we only request permission to post accepted abstracts on the workshop website.
  • Journal Special Issue:
    • Authors of selected accepted abstracts will be invited to submit extended versions for a journal special issue.

All submissions will be reviewed by members of the Program Committee. The paper review process is single-blind, which means that the author identities are not required to be anonymous and are visible to the PC members/reviewers, but reviewer identities are not visible to the authors. No special efforts are required to anonymize content in the paper (such as referencing the authors’ prior work).

Submission will be via the https://openreview.net/group?id=NFM/2026/Workshop/RExAI. To submit a paper on OpenReview, you must first create a profile and log in to the system.

A journal special issue that will contain the post-proceedings will be organized for extended, full papers corresponding to accepted abstracts.

Policy on the use of Gen AI - same as NFM: We understand the convenience afforded by the use of generative AI-based large language models to produce text in the submitted manuscript. However, we strongly encourage the authors to check the generated text for factual errors and inconsistencies. We encourage the authors to adopt appropriate standards for citing products obtained using generative AI (such as text, tables, graphics). Use of AI-based coding assistants is permitted, and we encourage authors to disclose the use of such tools as the community may find this scientifically interesting.

Remote Participation - same as NFM

While RExAI strongly encourages authors and attendees to join us in person, we recognize that travel to the United States can present challenges and that many valued members of the formal methods community reside abroad. For authors who are unable to travel, we will make every reasonable effort to support remote participation so they can present their work and fully engage with the symposium.

Organizers

Program Committee

TBD