LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software

• URL: http://arxiv.org/abs/2607.18555v1
• Date: Mon, 20 Jul 2026 22:41:55 GMT
• Title: LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software
• Abstract summary: We present an exploratory study on using Large Language Models (LLMs) to generate Alloy formal specifications.<n>We evaluate on two real open-source Python libraries: Flipper, a feature flag management system, and Cerberus, a data validation library.
• Score: 0.9023847175654603
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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 SD = 2.15) than documentation-based ones (mean SD = 5.0), though whether this generalises remains an open question. Index Terms--formal specifications, Alloy, large language models, automated testing, specification drift, software validation.

Related papers

• IntentTester: Intent-Driven Multi-agent Framework for Cross-Library Test Migration [14.0813614333238]
  We present IntentTester, a framework for intent-driven test reuse.<n>We evaluate IntentTester on nine open-source projects across three domains (JSON, HTML, and Time) and two languages (Java and Python)
  arXiv  Detail & Related papers  (2026-06-24T08:59:01Z)
• AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications [7.797719198801956]
  We introduce AssertLLM2, an open-source benchmark for realistic assertion generation in hardware verification.<n>AssertLLM2 contains 83 real-world designs across 13 functional categories.<n>For each design, the benchmark provides a structured design specification, a verified dependency-complete golden RTL, and systematically mutated buggy RTL variants.
  arXiv  Detail & Related papers  (2026-05-26T10:49:25Z)
• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  We introduce CodeSpecBench, a benchmark for executable behavioral specification generation under an execution-based evaluation protocol.<n>CodeSpecBench supports both function-level and repository-level tasks and encodes specifications as executable Python functions.<n>We observe a sharp performance degradation on repository-level tasks, where the best model attains only a 20.2% pass rate.
  arXiv  Detail & Related papers  (2026-04-14T04:31:45Z)
• GPT-4.1 Sets the Standard in Automated Experiment Design Using Novel Python Libraries [0.649540541957527]
  Large Language Models (LLMs) have advanced rapidly as tools for automating code generation in scientific research.<n>This study systematically benchmarks a selection of state-of-the-art LLMs in generating functional Python code.<n>Results show that only a small subset of models consistently generate correct, executable code.
  arXiv  Detail & Related papers  (2025-07-30T13:11:29Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  The paper introduces forward and backward constraints generation to improve the instruction-following capabilities of Code LLMs.<n>The authors present IFEvalCode, a multilingual benchmark comprising 1.6K test samples across seven programming languages.
  arXiv  Detail & Related papers  (2025-07-30T08:08:48Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$ is a high-quality, curated benchmark of 161 problems for end-to-end verified code generation in Lean.<n>Each problem consists of (1) the task of generating a specification that matches a held-out ground-truth specification, and (2) the task of generating a Lean implementation that provably satisfies this specification.
  arXiv  Detail & Related papers  (2025-05-20T05:15:47Z)
• METAMON: Finding Inconsistencies between Program Documentation and Behavior using Metamorphic LLM Queries [10.9334354663311]
  This paper proposes METAMON, which uses an existing search-based test generation technique to capture the current program behavior in the form of test cases.<n> METAMON is supported in this task by metamorphic testing and self-consistency.<n>An empirical evaluation against 9,482 pairs of code documentation and code snippets, generated using five open-source projects from Defects4J v2.0.1, shows that METAMON can classify the code-and-documentation inconsistencies with a precision of 0.72 and a recall of 0.48.
  arXiv  Detail & Related papers  (2025-02-05T00:42:50Z)
• DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts [7.019166148885954]
  We introduce DiffSpec, a framework for generating differential tests using prompt chaining.<n>We demonstrate DiffSpec's efficacy on two different (extensively tested) systems, eBPF runtimes and Wasm validators.
  arXiv  Detail & Related papers  (2024-10-05T18:11:14Z)
• GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
  We present GenAudit -- a tool intended to assist fact-checking LLM responses for document-grounded tasks.<n>GenAudit suggests edits to the LLM response by revising or removing claims that are not supported by the reference document, and also presents evidence from the reference for facts that do appear to have support.<n> Comprehensive evaluation by human raters shows that GenAudit can detect errors in 8 different LLM outputs when summarizing documents from diverse domains.
  arXiv  Detail & Related papers  (2024-02-19T21:45:55Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  Recent Language Models (LMs) have shown impressive capabilities in generating texts with the knowledge internalized in parameters. We propose to verify the output and the knowledge of the knowledge-augmented LMs with a separate verifier. Our results show that the proposed verifier effectively identifies retrieval and generation errors, allowing LMs to provide more factually correct outputs.
  arXiv  Detail & Related papers  (2023-10-19T15:40:00Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.