Enhancing Formal Software Specification with Artificial Intelligence

TL;DR

This paper demonstrates how integrating AI with lightweight formal specifications in natural language and LaTeX can improve software correctness, reduce effort, and facilitate early validation in industrial contexts.

Contribution

It introduces a novel approach combining AI and lightweight formal specifications in natural language to enhance software development efficiency and correctness.

Findings

Early validation of specifications achieved

Significant reduction in development effort

Correct implementation produced on first attempt

Abstract

Formal software specification is known to enable early error detection and explicit invariants, yet it has seen limited industrial adoption due to its high notation overhead and the expertise required to use traditional formal languages. This paper presents a case study showing that recent advances in artificial intelligence make it possible to retain many of the benefits of formal specification while substantially reducing these costs. The necessity of a clear distinction between what is controlled by the system analyst and can highly benefits from the rigor of formal specification and what need not be controlled is demonstrated. We use natural language augmented with lightweight mathematical notation and written in \LaTeX\ as an intermediate specification language, which is reviewed and refined by AI prior to code generation. Applied to a nontrivial simulation of organizational knowledge growth, this approach enables early validation, explicit invariants, and correctness by design, while significantly reducing development effort and producing a correct implementation on the first attempt.