PaperlayerView exact revision on arXiv

Source-linked AI summary

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

Aaron Councilman, David Jiahao Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, Vikram Adve

arXiv:2507.13290v2cs.PLcs.AI

TL;DR

LLM-generated code remains difficult to validate reliably for critical applications. The paper introduces a user-checked formal query language and verifier for Ansible, which verifies correct code in 83% of cases and identifies incorrect code in 92%.

  • Problem

    LLM-generated code and current validation techniques are not reliable enough for mission-critical or safety-critical applications.

    Source: §1 · pp. 1–2

  • Method

    Astrogator uses a natural language-like formal query that users can check, then verifies whether generated Ansible programs match that query.

    Source: §1 · p. 2, §4.1 · p. 7, §4.2 · p. 7

  • Results

    83% of cases had correct code formally verified, and 92% of cases with incorrect code were identified.

    Source: §1 · p. 3

  • Takeaways & Limitations

    Astrogator demonstrates formal verification of generated Ansible code against user intent and is presented as groundwork for systems that guarantee such matches.

    Source: §9 · p. 21

    68 of 70 incorrect programs accepted stemmed from under-specified queries and accepting any program that satisfied the query without human verification.

    Source: §6.3 · p. 17

Abstract

from arXiv · show

In the past few years LLMs have emerged as a tool that can aid programmers by taking natural language descriptions and generating code based on it. However, the reliability of LLM code generation and current validation techniques for it are far from strong enough to be used for mission-critical or safety-critical applications. In this work we explore ways to offer formal guarantees of correctness to LLM generated code; such guarantees could improve the quality of general AI Code Assistants and support their use for critical applications. To address this challenge we propose to incorporate a Formal Query Language that can represent a user's intent in a formally defined but natural language-like manner that a user can confirm matches their intent. We then have a formal specification of the user intent which we can use to verify that LLM-generated code matches the user's intent. We implement these ideas in our system, Astrogator, for the Ansible programming language, widely used for system administration, including for critical systems. The system includes an intuitive formal query language, a calculus for representing the behavior of Ansible programs, and a symbolic interpreter and a unification algorithm which together are used for the verification. A key innovation in Astrogator is the use of a Knowledge Base to capture system-specific implementation dependencies that greatly reduce the need for system knowledge in expressing formal queries. On a benchmark suite of 21 code-generation tasks, our verifier is able to verify correct code in 83% of cases and identify incorrect code in 92%.

1 Introduction

The paper addresses the difficulty of giving formal correctness guarantees to LLM-generated code when user intent is informal and testing is limited. It proposes user-validated formal queries and implements a verifier for Ansible, reporting results on 21 code-generation tasks.

1 Introduction

  • LLM-generated code can contain subtle errors, and mistakes in critical software can have disastrous impacts, motivating formal correctness guarantees.The paper notes that users can have difficulty checking generated code and that AI coding assistants have been associated with less secure code.Source: §1 · pp. 1–2
  • A natural-language prompt can be ambiguous or incomplete, while symbolic verification also requires formal semantics and a verification procedure that may be difficult to scale.Tests cover only a finite set of inputs and depend on test quality, so the authors argue they cannot provide complete correctness guarantees for critical systems.Source: §1 · p. 2
  • Astrogator uses a readable, formally defined query language that users can review, turning their intent into a specification for checking generated programs.The paper focuses its implementation on Ansible and discusses examples of applying the approach to Bash and a microcontroller language, leaving full verification systems for those languages to future work.Source: §1 · pp. 2–3
  • 83% of correct generated programs were formally proved correct, and 92% of incorrect programs were identified across 21 Ansible code-generation tasks.The authors attribute verifier failures to implementation and testing-set-up limitations rather than limitations of the overall approach.Source: §1 · p. 3

2 Background

The background introduces Ansible playbooks and illustrates how LLM-generated Ansible can fail through subtle, system-dependent mistakes.

2.1 Ansible

  • Ansible automates remote-system management; its YAML playbooks organize ordered tasks that invoke modules, as in the example that installs and starts Apache.A playbook runs on a controller that connects to managed systems over SSH.Source: §2.1 · pp. 3–4, Figure 1 · p. 4

2.2 Errors in LLM-Generated Ansible

  • LLM-generated Ansible can install the wrong package for an operating system or use a broad file-matching regular expression that replaces unintended environment variables.Detecting these errors can require knowledge of both Ansible and the underlying operating systems and package managers.Source: §2.2 · p. 4

3 Problem Statement

The paper models correctness as membership in the set of programs matching user intent, then explains why natural-language descriptions alone cannot support that determination. A formal specification enables program checking, but users must review both its fit to their intent and choices left unspecified.

3 Problem Statement

  • A program is correct when it belongs to the set of programs satisfying the user's intent, which may include many acceptable implementations.The user’s natural-language description does not provide a direct way to test membership in that set.Source: §3 · p. 5
  • A formal specification language gives descriptions formal semantics and makes it possible to decide whether a program satisfies the specification.The specification may be generated from the natural-language description, but ambiguous descriptions can yield a specification that does not match the user’s intent.Source: §3 · p. 5
  • Even a program satisfying the specification may differ from the user's intent through choices about details the description left unspecified.The verifier can present these choices as high-level assumptions for user review, but only the user can decide whether the program matches their intent.Source: §3 · pp. 5–6

4 Approach

The approach separates intent formalization, code generation, and verification: users check a natural-language-like formal query, which then serves as the specification for generated code. The verifier compares program behavior with that query and surfaces how the program fills in unspecified choices.

4 Approach

  • The proposed workflow uses a formal query and verifier as core components; an LLM may formalize intent, while code generation in this work uses the natural-language description alone.The user checks the formal query before code generation; the generated program need not satisfy it automatically.Source: §4 · p. 6

4.2 Program Verifier

  • Although the verifier can identify how programs resolve underspecification, the evaluation accepts every program that satisfies the formal query.The proposed design includes an Assumptions Check for users to review those choices.Source: §4 · p. 6

4.1 Design Considerations for a Formal Query Language

  • Because “copy a file” permits multiple interpretations, the user must review a natural-language-like formal query to check that it captures their intent.All six prompted LLMs generated code copying from the controller to the remote system in the example, despite other plausible meanings.Source: §4.1 · pp. 6–7
  • High-level descriptions such as “numpy” avoid requiring users to know implementation details; a knowledge base maps them to context-appropriate names.For Debian, the package name is python3-numpy.Source: §4.1 · p. 7

4.2 Program Verifier

  • The verifier checks whether a program matches the query and identifies its additional assumptions or actions for the user to review.For example, installing git before cloning is appropriate if the target machine lacks git, but may be unnecessary otherwise.Source: §4.2 · p. 7

5 Formal Query Language and Verification of LLM-Generated Code for Ansible

Astrogator implements a formal query language and verifier for Ansible. Its verification pipeline compiles queries and playbooks into the State Calculus, interprets their behavior symbolically, and unifies the resulting state pairs.

5.1 Ansible Formal Query Language Design

  • Its grammar structures queries as sentences of atomic actions or conditionals, with verbs, descriptions, and arguments.Figure 3 shows a fragment of the grammar; Table 2 gives examples of natural-language descriptions paired with formal queries.Source: §5.1 · pp. 8–9, Figure 3 · p. 8, Table 2 · p. 8
  • The query language aims to be understandable without specialized domain knowledge, preserving high-level descriptions rather than implementation-specific details.Queries follow a natural-language-like structure of sentences, atomic actions, and conditionals.Source: §5.1 · pp. 8–9

5.2.1 State Calculus.

  • The State Calculus models side-effecting programs as state transitions, representing attributes and object elements alongside reads, updates, deletion, and control flow.Its states can describe attribute values and whether objects such as files exist.Source: §5.2.1 · pp. 9–10

5.2.2 Symbolic Interpreter.

  • The symbolic interpreter explores possible initial states and tracks relevant state information, assigning symbolic values when reads encounter undefined attributes or elements.For symbolic conditions and case statements it explores both branches; for symbolic lists it executes a loop body once with a representative element.Source: §5.2.2 · pp. 10–11
  • For symbolic loops, the interpreter uses one representative list element, an imprecise approximation the authors consider adequate for Ansible’s simple loops.Source: §5.2.2 · p. 11

5.2.3 Program Verifier.

  • The unifier matches each query state pair to a program pair with consistent initial conditions and identical final states.Program initial conditions need not include every assumption made by the query, but required final behavior must match.Source: §5.2.3 · pp. 11–12
  • For underspecified queries, the unifier reports extra program assumptions and actions while still requiring every action specified by the query.Source: §5.2.3 · p. 12

5.3 Compiling Formal Queries to the State Calculus

Formal queries are compiled into State Calculus statements that represent their conditions and requested actions.

5.3 Compiling Formal Queries to the State Calculus

  • Conditional queries compile to if-then-else statements, with Boolean combinations of conditions represented as pure functions.Source: §5.3 · p. 12
  • Base conditions, such as checking the operating system or file existence, compile into code that reads and checks the corresponding state attributes.Source: §5.3 · p. 13
  • Atomic actions compile according to their verb and description; for example, creating a file adds a file element and sets its argument-specified attributes.The supported verb set is currently built into the compiler, though the authors believe it could be made extensible.Source: §5.3 · p. 13

5.4 Compiling Ansible Programs to the State Calculus

Astrogator compiles Ansible playbooks and formal queries into the State Calculus using module definitions for types and behavior. A knowledge base lowers high-level query descriptions into implementation-specific details.

5.4 Compiling Ansible Programs to the State Calculus

  • Playbook compilation translates tasks in sequence, representing modules as stateful function calls and handling conditions, returned values, and loops.Constructing correctly typed module inputs and translating built-in variables into state-attribute reads are the main complexities.Source: §5.4.1 · p. 13, §5.4 · p. 13

5.4.1 Ansible Playbook to State Calculus Compiler.

  • Because module documentation and implementations do not adequately provide the needed type and behavior information, the authors define a language for module specifications.The language supports optional and mutually exclusive arguments, enumerated values, and defining state elements and attributes.Source: §5.4.2 · p. 13

5.4.2 Module Description Language.

  • The copy-module description handles required dest, exclusive src/content, and optional remote_src arguments, then specifies source-file and destination-content behavior.The description can track file paths and systems without modeling hard links correctly at that coarse level.Source: §5.4.2 · pp. 13–14, Figure 5 · p. 14

5.5 Formal Query Language Knowledge Base

  • The knowledge base maps high-level package and file descriptions to lower-level details using context, such as OS-specific package names and managers.Its functions are hand-curated and can be replaced or extended through an interface parameterizing the compiler.Source: §5.5 · pp. 14–15

6 Evaluation

The evaluation tests Astrogator on a 21-task Ansible benchmark and 1,260 LLM-generated programs. It measures verifier accuracy, characterizes generated-code quality, and examines the sources of verifier errors.

6.1 Benchmark Suite

  • The 21 benchmarks cover common Ansible tasks, with reference solutions averaging 1.67 tasks and reaching a maximum of four.Correctness was judged against tests on virtual machines running Debian, Ubuntu, and RHEL; a program had to pass all tests on every tested system.Source: §6.1 · p. 15

6.2 LLM Code Generation

  • Across six LLMs prompted for ten programs per task, only 334 of 1,260 generated programs (26.5%) were correct; GPT-4o reached 51.4%, versus 21.5% for open-source models.Table 3 categorizes model outputs by syntax errors, execution errors, test failures, and correct programs.Source: §6.2 · pp. 15–16, Table 3 · p. 17

6.3 Verifier Accuracy

  • Astrogator accepted 277/334 correct programs (82.9%) and rejected 856/926 incorrect programs (92.4%) across 1,260 samples.The benchmark-level results are presented in Table 4.Source: §6.3 · p. 16, Table 4 · p. 17
  • Verifier errors include false rejections from unsupported features or single-response knowledge-base entries, and false accepts often reflect under-specified queries or assumptions users must review.The authors characterize these errors as addressable through implementation changes or user input.Source: §6.3 · pp. 16–18

7 Discussion

The discussion describes Astrogator’s engineering demands and illustrates how the State Calculus can verify hand-translated programs beyond Ansible. These examples remain bounded by language-specific support and modeling choices.

7.1 Engineering Effort

  • Astrogator required significant development effort, and the authors identify that effort as a possible barrier to adoption.They propose future automation of components including the Knowledge Base, parts of the Formal Query Language, and module specifications, with manual review of generated components.Source: §7.1 · p. 18

7.2 Generality

  • The State Calculus and symbolic interpreter may support verification of other stateful languages, with Bash and Arduino examples extending beyond Astrogator’s Ansible-specific implementation.The authors say these examples suggest potential for other similar languages, while leaving expanded language support for future work.Source: §7.2 · pp. 18–19
  • Astrogator verifies a hand-translation of a Bash script against a hand-written specification, including constructs such as redirects, pipes, and file descriptors.The example uses definitions of the Linux utilities involved; arbitrary while-loops and more complex loops are not supported by the described handling.Source: §7.2 · p. 19
  • For Arduino, the example verifies that a hand-translation of the program’s main loop matches a hand-written specification at each step.The authors note verification may need to be paired with other techniques to establish expected invariants, including assumptions about globals.Source: §7.2 · p. 19
  • In both examples, source translation is described as straightforward, while language specifications and state representation remain important work.The Bash example relies on utility definitions; the Arduino example relies on built-in function specifications, and both use hand-translations.Source: §7.2 · p. 19

8 Related Work

Related work includes controlled natural languages, testing and verification of generated code, natural-language program summaries, formal-specification generation, and program synthesis. The paper positions its formal queries as user-checkable specifications for LLM-generated code.

Controlled Natural Languages

  • Formal Query Languages resemble controlled natural languages, which have been used for database queries and logic specifications; the authors know of no prior use for formalizing intent in LLM code generation.The authors say this similarity bolsters their belief that users can understand formal queries.Source: §8 · pp. 19–20

Identifying Incorrect LLM Generated Code

  • Testing generated code depends on users crafting good tests, while proof-assistant approaches require formal theorem statements and do not generalize to general code.The cited discussion notes errors in ground-truth HumanEval solutions despite their tests.Source: §8 · p. 20

Natural Language Summaries

  • Prior natural-language program summaries help users judge intent, but the authors argue high-level specifications better guard against summaries that seem reasonable despite subtle errors.The cited summary work is marked [8].Source: §8 · p. 20

LLM Generation of Formal Specifications

  • Prior LLM-generated formalizations include post-conditions and Isabelle statements, but the authors consider them too low-level for users to check against natural-language descriptions.The cited work includes and [42].Source: §8 · pp. 20–21

Program Synthesis

  • The paper connects its envisioned code-generation loop to counterexample-guided synthesis and interactive synthesis, and discusses Photoscout [8] as related work combining LLMs and synthesis.The authors suggest formal queries could provide a basis for synthesis in Ansible.Source: §8 · p. 21

9 Conclusion

The conclusion presents formal query languages as a way to formalize user intent and check LLM-generated code. Astrogator demonstrates the approach for Ansible, while its verifier remains imperfect.

9 Conclusion

  • The paper proposes formal query languages to formalize user intent and check LLM-generated code for correctness.It presents design constraints intended to help users check that a query matches their intent.Source: §9 · p. 21
  • Astrogator implements the approach for Ansible and shows that its verifier can identify correct and incorrect generated code, though the verifier is imperfect.The authors attribute observed errors to limitations in the testing setup or implementation.Source: §9 · p. 21
  • The authors present the work as groundwork toward code generated from natural language that is guaranteed to match user intent, which they call essential for AI Code Assistants in critical systems.Source: §9 · p. 21

A Benchmark Suite Natural Language Descriptions and Formal Queries

The appendix presents natural-language descriptions alongside formal-query examples for system administration and configuration tasks. The examples cover operating-system conditions, users, services, files, permissions, and software environments.

A Benchmark Suite Natural Language Descriptions and Formal Queries

B LLM Code-Generation Prompt

The prompt directs an Ansible expert to generate a playbook from a task description and return only the playbook content. It explicitly prohibits shell and command modules.

B LLM Code-Generation Prompt

Related papers

Loading 2507.13290v2…