Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This study explores the use of Large Language Models (LLMs) to generate Alloy formal specifications from requirements documentation and production source code, enabling the automated derivation of executable test cases. Evaluating on two open-source Python libraries, Flipper and Cerberus, the LLM-generated specifications not only produced valid tests without manual correction but also uncovered previously undetected bugs, highlighting the limitations of traditional test generation methods. The findings indicate that incorporating a formal intermediate representation can reveal constraint-level defects that standard coverage-oriented approaches may overlook, with code-derived specifications demonstrating more consistent test generation than those based on documentation.
LLM-generated Alloy specifications can uncover critical bugs that traditional test generation methods miss, revealing a significant gap in current testing practices.
We present an exploratory study on using Large Language Models (LLMs) to generate Alloy formal specifications from both requirements documentation and production source code, and to derive executable test cases from those specifications. We evaluate on two real open-source Python libraries: Flipper, a feature flag management system, and Cerberus, a data validation library. In both cases, the LLM produced workable Alloy specifications and executable tests without any manual correction. For Flipper, our pipeline uncovered a genuine bug that the existing test suite had missed: the library silently accepts duplicate flag names, directly contradicting its documented uniqueness requirement. A direct LLM baseline—generating tests from the same README but skipping the Alloy step—achieved $68\%$ branch coverage yet failed to catch this bug across all three independent runs. This suggests that introducing a formal intermediate representation can surface constraint-level defects that coverage-oriented generation may miss. For Cerberus, the code-derived specification captured an implicit abstraction over sized types that the documentation-derived spec omitted, producing two additional tests. Across both libraries, code-based specifications showed lower variance in test generation (mean $\mathrm{S D} {=} {2 . 1 5}$) than documentation-based ones (mean SD = 5.0), though whether this generalises remains an open question.