Abstract
<jats:p>The development of safety- and mission-critical software has traditionally relied on formal methods to guarantee correctness, consistency, and verifiability. Despite their proven benefits, their use in mainstream software engineering remains limited due to the need for strong mathematical expertise, longer development times, rigid tools, and the absence of a large practitioner community. The emergence of artificial intelligence (AI) opens new possibilities to simplify formal development and encourages a revision of computer engineering curricula. This article proposes integrating the formal metamodeling language Nereus with AI throughout the software lifecycle. Current research explores how large language models (LLMs) such as ChatGPT can analyze, complete, and generate algebraic specifications, supporting syntactic and semantic reasoning, rewriting, and simulation. The article presents experiments redesigning an introductory algorithms and data structures course under this approach and introduces a metacognitive strategy to reinforce formal education in the AI era.</jats:p>