arXiv CSopen access

Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming

Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming Ziqi Yuan† , Wenhao Lu† , Hao Wu, Dunhong Jin, and Chuan Wu

arXiv:2607.02333v1 [cs.SE] 2 Jul 2026

The University of Hong Kong [email protected], [email protected], [email protected], [email protected], [email protected] † Equal contribution

Abstract—Vibe coding democratizes software development by allowing users to generate code via natural-language (NL) interaction with large language models (LLMs). However, the code is reliable only when it faithfully implements the user’s intent, which is difficult and labor-intensive for users to validate, especially for non-programmers. Existing validation methods either rely on LLM-assisted automated testing, which suffers from prompt ambiguity and model fallibility, or involve users only in partial software artifacts such as prompts and test cases, which may overlook corner cases and program details. Motivated by a bug study of LLM-generated code, we find that detailed human feedback is essential, as the failures often stem from underspecified requirements or subtle semantic deviations, and thus cannot be resolved through automated or coarse-grained checking alone. This paper presents verifiable literate programming (VLP), a human-in-the-loop framework designed to make the review/validation process of LLM-generated code accessible to users at all programming levels. At its core, VLP proposes unambiguous NLbased documentation as a readable intermediate layer between prompts and code. The documentation demonstrates concrete program semantics and enables users to provide feedback on potential intent-code mismatches. It supports human-involved, end-to-end repair and validation via three techniques: (i) an NL-style literate language with unambiguous syntax and mostly deterministic code-to-documentation translation, (ii) LLM-based fine-grained mismatch detection that uses trace links between prompts and documentation to focus users’ review effort on suspicious documentation lines, and (iii) a verification module that leverages user-validated documentation to derive API-usage checks and formal properties, which are then verified against the generated code using model checking. Our evaluation shows that VLP improves code pass@1 from 28.7%–73.2% to 65.4%–93.5% with reasonable user effort.

I. I NTRODUCTION Vibe coding democratizes software development by shifting much of programming from manual code writing to naturallanguage (NL) interaction with large language models (LLMs). As a result, recent reports estimate that 63% of vibe-coding users are non-programmers [1], [2]. However, LLM-generated code is useful and trustworthy only when it faithfully implements the user’s intended behavior. Ensuring intent-code alignment is difficult because LLMs can hallucinate during generation, while users, especially non-programmers, often face many lines of generated code without knowing whether the program actually behaves as intended. This concern is reflected in recent developer surveys, which report that LLMgenerated code remains unreliable [3]–[5] and that 96% of

developers do not fully trust the functional correctness of AIgenerated code [6]. Therefore, validating LLM-generated code has become an urgent problem for vibe coding. This need has motivated a large body of work on automated testing and verification for LLM-generated code. One line of work utilizes LLM reasoning to generate tests or formal properties from the original NL prompt, or to directly judge program correctness [7]–[19]. However, these methods suffer from the ambiguity of the original prompt and the fallibility of LLM-generated validation artifacts. Tests may miss important paths, formal properties tend to overlook key requirements, and LLM-based judges can misjudge correctness [20]–[23]. Thus, validation that depends solely on LLM reasoning cannot provide a fully reliable basis for LLM-generated code. Recognizing these limits, recent work has begun to involve users in specific stages of the vibe coding workflow to align code with user intent. Clarification-based methods ask users to resolve ambiguous prompts before code generation [24]– [29], while test-driven interaction methods use user feedback on generated test cases to partially formalize intent [10], [30]–[32]. These methods can expose ambiguities or concrete program failures, but they involve users only through partial software artifacts. Prompt clarification cannot catch errors introduced during code generation, and test cases cover only sampled behaviors, potentially missing subtle deviations and corner cases [20], [21]. Test-case-based code validation can also be hard for data-science and domain-specific programs, where outputs are often statistical, data-dependent, and difficult to judge from input/output examples alone [33], [34]. Ideally, an effective validation workflow should help users find and repair more intent-code mismatches with minimal effort. To understand what failures in LLM-generated code should be exposed to users and how to effectively interact with users, we conduct a bug study on BigCodeBench-Hard [35] using DeepSeek V4 Flash [36] and Claude Opus 4.7 [37]. We find that most failures stem from underspecified prompts or subtle semantic deviations, necessitating fine-grained user judgment beyond automated checking. In addition, 81.7%– 83.3% of the studied failures can be expressed as concrete intent-level behavior in NL. These observations and literate programming [38] together motivate our key idea of verifiable literate programming (VLP). As illustrated in Figure 1(b), VLP introduces NL-based program description (called documentation) as a faithful and readable intermediate layer between

user feedback for repair

user intent and generated code. The layer is literate because (a) Literate programming Documentation interleaved with code it exposes the concrete semantics of LLM-generated code in Literate program (source) WEAVE Documentation a form that users can read without programming-language (typesetting) # copy each file to the output dir human-readable prose knowledge. It is verifiable because the documentation is linked # if the name exists, rename it to the code through (mostly) bidirectionally deterministic codeSource code TANGLE for f in files: (code extraction) def copy_files(...): ... to-documentation translation. Once validated by users, it can be if exists(d): d = uniq(d) translated into formally verifiable properties and deterministic Ours (b) Verifiable literate programming (VLP) code aligning with user intent. To realize this idea, VLP targets three connected design NL prompt Python code (snippet) goals. First, documentation must be faithful and unambiguous: LLM Copy each file to the output if exists(target): if the documentation is merely a lossy LLM-generated summary target = uniq(target) folder. If the name exists, copy(f, target) rename it; otherwise copy as is. or comment [39], [40], subtle deviations and underspecified behaviors in the generated code may disappear before users A: Code-derived literate documentation faithful, unambiguous NL If the file called target already exists, target = uniq(target) ！ can inspect them. Second, validation must be low-effort: even Copy the file f to target faithful documentation is impractical if users must review it line Literate Properties: No existing file is overwritten by line, so VLP should guide users to snippets most likely to require intent validation. Third, validated documentation must B: User validation Take Suggestion Keep Doc Comment lead to reliable code: without translating validated or repaired Find suspicious documentation lines for review: “On a name clash: what is the specific renaming rule of the target file?” documentation into reliable code, users would still need to reason about whether the code aligns with the documentation C: Automated verification and whether programming-language-specific issues exist, such Bounded model checking of properties (if any) Python API-usage checks (os.path, shutil) as API usage and syntax. VLP realizes these goals through three components. First, Validated and verified Python program Verifiable it introduces an NL-style literate language (§IV-B) that uses syntax-directed translation to turn generated code into strucFig. 1: Conventional literate programming workflow versus tured, human-readable descriptions. Meanwhile, it preserves the verifiable literate programming (VLP) workflow. In VLP’s user control flow, data flow, and assertion-based properties. Second, validation, Take Suggestion confirms the detected mismatch VLP provides misalignment hints through implementationor proposed fix, Keep Doc retains the original documentation, relevant traceability and taxonomy-based mismatch detection. and Comment indicates the user will clarify the intent. The trace links are built between implementation-relevant senloop validation framework for LLM-generated code. VLP tences or formulas in the prompts and the documentation. Given first translates generated code into faithful, readable, and finethese linked sentences and their surrounding context, LLMs can grained literate documentation; then uses trace-link-guided more accurately flag intent-documentation mismatches. Then, LLM analysis to find likely intent-documentation mismatches VLP highlights suspicious documentation snippets for user for user validation and repair; and finally uses the validated feedback (§IV-C). Third, it derives API checks and formal documentation to derive verifiable properties and API usage properties from the validated documentation and verifies them checks for verifying the generated code. against the generated code with bounded model checking [41]. We encourage users to focus on intent-level decisions and let • We evaluate VLP on two coding benchmarks and show that it helps users validate and repair LLM-generated code more VLP automatically handle Python-specific details (§IV-D). effectively (i.e., higher pass rate) than SOTA human-in-theWe build a VLP prototype. Our evaluation on QuantCodeEloop code generation and validation methods. val [34] and BigCodeBench [35] examines whether VLP helps users effectively identify intent-code mismatches in LLMII. BACKGROUND generated code and improves code correctness. The results show that VLP improves pass@1 from 28.7%–73.2% to 65.4%– A. Literate Programming 93.5%, significantly outperforming the original generated Literate programming [38] was introduced with the philosocode and three state-of-the-art (SOTA) human-in-the-loop phy that programs should be written for humans to read, not code generation methods: ClarifyGPT [24], TiCoder [32], and only for machines to execute. Instead of organizing a program PInG [40]. Our user study further shows that VLP achieves solely around compiler requirements, literate programming higher user experience and provides better tradeoff between asks programmers to present the program in an order and user validation time and code correctness. In summary, we form that explain the underlying ideas to human readers. As make the following contributions. shown in Figure 1(a), in the original literate programming • We conduct a systematic bug study of LLM-generated code system, a programmer interleaves explanatory text with code. on BigCodeBench-Hard. Our study shows that most failures The WEAVE processor then produces readable documentation, can be reviewed by users as intent-level misalignments while the TANGLE processor produces executable code. through an NL representation of program semantics. Although literate programming is not widely adopted today, • We propose verifiable literate programming, a human-in-the- its core idea has had broad influence. Modern computational

notebooks, such as Jupyter notebooks [42], continue this idea by placing explanations, code, and results in the same document. Although VLP, shown in Figure 1(b), is inspired by the readable documentation layer of literate programming, the two differ in several aspects. First, VLP’s documentation is derived from the code in a mostly deterministic and unambiguous way, rendering it more faithful to the code semantics than the free-form explanatory prose used in conventional literate programming. More importantly, literate programming uses NL primarily to support human comprehension. In contrast, VLP uses NL as part of a review and validation process. It assesses whether generated code implements user intent and helps identify underspecified requirements in the prompt as well as deviations in the code. B. Formal Verification Tools Beyond improving program readability for human review, formal verification tools also play an important role in ensuring code correctness. When part of the intended behavior can be expressed as explicit formal properties, bounded model checking (BMC) [41], [43] can automatically check whether a program satisfies those properties over all feasible executions up to a given bound. If a symbolic execution path reaches a violation state, the checker returns a concrete counterexample, including the input and the execution path that break the property. Otherwise, within the bounded search space explored by the checker, the property holds for all feasible executions. Compared with unit testing, BMC provides stronger assurance. Unit tests exercise only selected concrete inputs, whereas BMC reasons over symbolic inputs and systematically explores feasible execution paths. Although BMC does not prove correctness beyond the chosen bound, it is often more automatic and lightweight than full deductive verification while providing stronger guarantees than ordinary testing. At the same time, though formal tools can verify code with respect to a given property, they do not determine whether that property faithfully reflects the user’s intent. In particular, they cannot by themselves identify underspecification in the original prompt or detect cases where the code satisfies the written property while still subtly deviating from user intent.

Logic-Related

Python-Specific

10 12

Missing Steps

Wrong API 1 4 Call

22

Redundant Steps

10 9

Wrong Execution Flow Wrong Action/Operation

Wrong API Call Sequence

16 19

Lacking Domain Knowledge Prompt Underspecification

79

Other Python Issues

12 6

0

14

50

Count

DeepSeek Easy DeepSeek Hard

9 2 5 10

Missing Exception Handling

68

Other Logic Issues

4

Wrong API Arg Value

6 5

Wrong Operand Value

4

Wrong API Arg Type

20 13 13

100

Opus Easy Opus Hard

10 4 2

0

10

Count

20

DeepSeek Python Opus Python

Fig. 2: Bug taxonomy of code generated by DeepSeek V4 Flash and Claude Opus 4.7 using BigCodeBench-Hard [35]. Note that when a prompt only omits background knowledge or conventions that are generally expected within the task domain, we categorize the related bug as Lacking Domain Knowledge rather than Prompt Underspecification. Specifically, we focus on BigCodeBench-Hard Instruct mode [35], which contains complex instructions and diverse library usage. We prompt Claude Opus 4.7 and DeepSeek V4 Flash (temperature=0.2). To investigate the opportunity of NL-based documentation, we further translate each generated program into NL documentation using the approach introduced in §IV-B. Across 148 tasks, each with approximately five tests, we collect about 200 bugs from each model [36], [37]. For each bug, two experienced programmers independently inspect the task description, test cases, error message, generated code, and corresponding documentation, and label whether the bug is reviewable in the documentation. Disagreements are resolved through discussion. A. Observations from the Bug Study

Most failures are reviewable at the intent level in NL and not solvable via automated checking. We first examine whether failures in the generated code can be exposed by translating code behavior into NL descriptions (documentation). We consider a bug documentation-reviewable if its incorrect behavior can be recognized from the documentation, without requiring users to inspect Python-specific details such as syntax, package imports, complex data types, or library usage. As III. B UG S TUDY AND M OTIVATION FOR VLP shown in Figure 2 (Logic-Related), most studied bugs are We conduct a bug study to figure out what failures in LLM- documentation-visible: 156 out of 191 bugs for DeepSeek generated code should be exposed to users and how to interact and 169 out of 203 bugs for Opus. This result suggests that with users. Specifically, Python is chosen as the programming documentation can expose a large fraction of failures at the language for our study and system implementation because of intent level. Moreover, 85.9%–90.5% of documentation-visible its widespread use. We find that failures frequently arise from bugs are easy for users to judge because the incorrect behavior underspecified requirements or subtle semantic deviations and can be identified from the problematic documentation line and a therefore cannot be resolved by automated or coarse-grained few surrounding lines, without reading the full documentation. checking alone. Detailed NL documentation and concrete Failures require fine-grained review of underspecification validation questions about short documentation snippets for and subtle semantic deviations. Generated code usually users can expose these deviations, allowing users to confirm follows the overall prompt, but many reviewable failures come the intended behavior. Our observations motivate VLP’s from underspecified or subtle details. Prompt underspecification documentation-based user interface that (i) enables users to is the largest source, accounting for 43.6%–46.7% of reviewable validate program semantics in NL and (ii) provides precise bugs. Across these cases, the LLM makes plausible choices guidance for user feedback. according to its assumptions rather than confirmed user intent.

For example, an LLM may filter records that the user expects to the literate language (§IV-B), which converts generated code keep, or silently return a fallback value instead of reporting an into human-readable descriptions via syntax-directed translation. error. The remaining reviewable failures often involve missing VLP also presents the documentation hierarchically, so users steps, redundant steps, wrong execution flow, wrong actions or can keep the global overview while diving into local details. operations, and wrong operand values. Overall, we observe that (2) VLP recovers trace links between the documentation and many reviewable failures are subtle. Concretely, the generated implementation-relevant sentences in the user prompt, allowing code mostly follows the prompt, but it instantiates a slightly LLMs to identify potential mismatches more accurately by different intent that requires fine-grained review and validation. narrowing the search scope. The mismatch-detection prompt Intent-level documentation cannot support reviewing is guided by the bug taxonomy derived from our study. Python-specific failures. As shown in Figure 2 (Python- When a potential mismatch is detected, the LLM generates Specific), failures that are not documentation-reviewable typ- concrete validation questions about the intended behavior ically result from programming-language-level bugs that are and presents them to users with the surrounding context difficult to express as user-facing intent, such as API selection, (§IV-C). (3) VLP integrates automated tools to check API argument meanings, return-value handling, and side effects. usage and algorithmic properties in the generated code against API calls are a typical case. Documentation can record the the validated documentation (§IV-D), which reduces the burden callee, arguments, and return target, but judging whether they of manually reviewing complex algorithms and Python-specific implement the intended action often requires library knowledge. implementation details. These failures are difficult to validate through documentation alone, especially for non-programmers with limited library A. Workflow of Verifiable Literate Programming As shown in Figure 3, VLP consists of a code generation knowledge or programming expertise. step followed by a multi-turn review-and-repair loop until the B. Design Goals documentation is validated by the user. Then, the code will go The observations above motivate the central idea of VLP: through API check and assertion-based property verification. using NL-based documentation as a faithful and readable interGeneration step. Given an NL prompt (➀), VLP first mediate layer between user intent and generated code. For users, generates Python code, where the LLM is encouraged to this layer exposes the concrete semantics of LLM-generated generate assertion-based properties alongside the code (➁). code in a form they can review even without programming- Then, it applies Python-to-documentation translation (➂). language knowledge. For reliable code generation, VLP turns Mismatch detection for guiding user review and validaconfirmed user intent into program repair targets and verifiable tion. After the documentation is constructed, VLP analyzes properties. Based on this idea, VLP has three design goals. documentation-intent alignment (➃). It decomposes the prompt First, the code-to-documentation translation must be faithful and the documentation into fine-grained alignment units and and unambiguous enough to demonstrate subtle deviations and recovers trace links between them. Based on the linked pairs, underspecified behaviors in LLM-generated code. It should VLP uses an LLM to detect and potential intent-documentation never use ambiguous NL sentence structures that confuse users mismatches in a fine-grained manner. These problematic or lose important program semantics, including control flow, documentation snippets are highlighted in the user interface data flow, and assertion-based properties. with related validation questions and evidence from the prompt, Second, VLP should minimize user effort in documentation which turns a long documentation review into a focused set review. Though many failures can be exposed, users cannot be of intent-level validations. If the user revises a highlighted expected to review the entire documentation. Instead, an effi- snippet, VLP patches the Python code accordingly (➁) and cient framework should present users suspicious documentation updates the corresponding documentation lines (➂). snippets and provide precise surrounding context. Complementary verification after user validation. After Finally, after multi-turn user review and repair, the validated the documentation is validated, VLP checks the remaining documentation should help turn user-confirmed intent into details that are better handled by automated formal verification reliable Python code. In vibe coding, users should not be methods. It uses bounded model checking (➄) for two comresponsible for checking Python-specific details or low-level plementary tasks: (i) Python-specific checking for library calls implementations of complex algorithms, as these details are and related implementation details, and (ii) property checking hard to verify manually. Fortunately, the documentation retains stated as NL assertions in the documentation. If verification assertions and concrete NL descriptions of API behaviors. Thus, fails, VLP feeds the failure examples back into the repair VLP can use automated verification tools to check assertion- loop. The workflow terminates once the Python code passes based properties and API usage against the generated code. verification or the maximum repair count is reached. IV. D ESIGN

B. Literate Language Design and Documentation Construction

This section first presents the overall workflow of VLP (§IV-A) and then describes the design of three components that help users repair and validate LLM-generated code. (1) VLP introduces an NL-style language for the documentation called

To translate generated code into literate-language documentation, first, we design grammar and conversion rules to support (mostly) deterministic translation for validation-relevant code snippets. Second, we encourage the code-generation LLM to

Loop on user feedback (repair ) 3

1

NL prompt

2

Python generation

Code-derived NL documentation code to readable NL

4

User validation user reviews flagged lines

Syntax-directed Python-to-documentation translation (Sec IV.B) Python code (buggy API) def copy_files(files, out): for f in files: dst = join(out, f.name) if exists(dst): rename(f, dst) copy(f, dst)

For each f in files Join the OS path of out and f.name then return to dst If the file dst already exists, rename the file f to dst Copy the file f to the path dst

test omitted

trans rule for if

body

func: rename

Rule: T(If(test=t, body=[a])) = "If " + T(t) + ", " + T(a) Doc: If the file dst already exists, rename...

expr trans rule Rule: T(Expr(APICall(func=v, args=[a1, ..., an]))) =

call for API call arg: f

arg: dst

validated & verified

NL prompt

1

Code-derived documentation

Extract impl-relevant prompt skeleton

2

Decompose prompt into sentences/formulas

3 Impl-relevant TLR

Fine-grained misalignment detection over linked prompt and documentation

Syntax-directed Python-to-documentation translation

if

6 Final accepted code

Fine-grained misalignment detection based on TLR (Sec IV.C)

Literate-language documentation

Translate

if exists(dst): rename(f, dst)

5 Python-level checking model checking & API checks

Realize(F_v, T(a1), ..., T(an)), where F_v = [literate verb phrase slots over a1, ..., an] LLM: F_rename(src, dst) = "rename the file {src} to {dst}" Doc: rename the file f to dst

Literate-language documentation # ...

If the file dst already exists, rename the file f to dst # ...

Intent mismatch

Prompt sentence x: If a file name conflicts in the output folder

Prompt sentence y: Rename the new copy of the file

X

LLM detection

The program moves source f to dst and may overwrite dst.

Underspecification What renaming rule should file f follow?

Fig. 3: Workflow and major components of VLP, where the original code is buggy and the prompt is underspecified. TABLE I: Selected literate language syntax categories, their purposes, and examples. Categories

Purpose

Example

Declarations and type signatures

Introduce functions, custom types, fields, inputs, and outputs in a form close to English.

There is a calculate_score function, whose input is a decimal named raw_val, whose output is a decimal

Core expressions and data access

Express arithmetic, Boolean logic, etc. Prefer keeping symbolic representations as users are familiar.

today_score = basic_score + correct_answers[date, person_id] / 2

Programming-style function calls

Support precise function invocation inside expressions, including recursion and method calls.

recursive_calc(n - 1) + recursive_calc(n - 2) + 1

Natural-language-style operations

Describe workflow steps and API-like operations as verb phrases, optionally with parameters and returns.

Normalize input_values with scale = 2.0 then return to normalized

Conditionals and predicate formulas

Encode branching logic using either comparison expressions or restricted natural-language predicates.

If (volatility_index exceeds threshold by 10 percent) and (min_score > 50), is_valid = true

Loops and iteration

Express both conventional loops and natural-language iteration over collections.

For each document in document_collection, extract keywords from document and append to kw_list

Properties assertions (Hoare logic style [44])

State preconditions and postconditions for verification inside formally declared functions.

At this point, assume that unsorted_score_list.length >0

summarize complex algorithm implementations by extracting their properties, so users can simply review high-level behavior and automated checks can subsequently verify low-level details. Third, we organize the documentation into a hierarchical structure when showing it to users, preserving a global overview while enabling rapid comprehension of the local context. At the language level, we define the literate language with an NL-style LALR(1) grammar, a parser-friendly grammar with an unambiguous parse structure. This keeps the documentation readable to users while remaining precise enough to review. In this paper, we use English in the literate language and study 200 NL-program pairs, together with prior NL-programming literature [45], [46], to analyze how people express programminglanguage semantics in English. Nevertheless, VLP can be extended to other natural languages by building dedicated LALR(1) lexers and parsers. Syntax-directed python-to-documentation translation. For major Python syntax rules, we propose corresponding

translation rules in the literate-language grammar. As shown in Table I, these rules follow Python’s key syntactic categories, including declarations, expressions, function calls, conditionals, loops, and assertions. During runtime, after an LLM-generated Python program is parsed into a syntax tree, VLP performs a syntax-directed translation. It traverses the tree and emits literate-language snippets following the corresponding translation rules. During translation, several hierarchical Python syntax-tree nodes often need to be linearized into one literatelanguage sentence. We therefore carefully design the literatelanguage syntax so that such sentences read naturally while still preserving the nested grammatical structure needed for LALR(1) parsing. Specifically, step ➂ in Figure 3 illustrates how a complex Python statement is translated by fixed rules into a literate-language sentence step by step on the tree. Ideally, the translation would be fully deterministic even though Python syntax supports flexible parts such as variable names and expressions. In most cases, this is possible

because the translation rules directly carry Python variable do not know which parts of the long documentation deserve names, expressions, and conditions into the corresponding more attention. To narrow the scope, as illustrated in step ➃ of documentation without decimating readability. However, some Figure 3, VLP conducts fine-grained misalignment detection flexible parts cannot be handled by syntax-directed translation based on implementation-relevant trace links between docualone. Simply copying these Python snippets would make the mentation and prompts, and then presents found mismatches documentation hard to read, yet their forms are too flexible for and corresponding validation questions via the user interface. us to exhaustively define fixed rules that translate them into Implementation-relevant traceability link recovery. VLP understandable literate-language descriptions. API calls are a detects mismatches by comparing linked pairs of prompt-side typical case. The converter can parse the callee, arguments, and and documentation-side link units. Each unit covers a single return target, but the API name often needs to be explained as action, a condition, a function signature, or a formula, including a clearer action, such as creating a dataframe or computing a constants and literals. For example, a sentence in the prompt distance matrix. Likewise, lambda expressions and higher-order describing how invalid inputs should be handled should be expressions may encode sorting keys, filtering rules, or data linked to the code snippets that implements the check and transformations. A fixed translation rule would either stay too corner-case handling. Such fine-grained links have two benefits. close to raw Python or miss the behavior users need to validate. First, they allow the LLM to focus on a specific bug type VLP therefore statically analyzes syntax trees and marks and a small snippet in each detection step, following the these snippets as python_level blocks. For each python_level general principle of decomposing complex tasks into focused block, the LLM generates a short verb phrase using its subproblems [47], [48]. Second, the narrow scope makes the pretrained knowledge and available docstrings. Meanwhile, for detected mismatches easier for users to review. determinism, translation rules still fix the surrounding control We regard this as a traceability-link recovery (TLR) probflows, input arguments, and return assignment. lem [49] with an implementation-relevance filter, which we Property support in documentation. Reviewing every refer to as implementation-relevant TLR. Our design is motiimplementation step of a complex algorithm can make user vated by the observation that complex coding prompts often validation difficult. Therefore, VLP encourages the Python- contain implementation-irrelevant noise, such as explanatory generation LLM to abstract algorithms into compact properties. sentences and background information. Thus, instead of treating We use assertion-based Hoare-logic-style properties: a pre- all prompt sentences as link candidates, VLP identifies the condition specifies what must hold before function execution, behaviors and constraints that a correct implementation must rea postcondition specifies what must hold after the function alize and builds link units around them. Specifically, the prompt returns, and an invariant specifies what must remain true side and the documentation side are selected and decomposed during execution. For example, a sorting function can be differently. For documentation, where program structure is documented by requiring the output to be ordered and to contain available, VLP uses syntax trees to identify candidate link the same elements as the input, rather than describing each units such as verb-phrase statements, conditions, properties, implementation step. Such properties serve as a shared interface formulas, and basic blocks. These units expose the concrete between users and verification tools. In VLP, users validate actions and conditions expressed by the implementation. On the prompt side, VLP uses an LLM to decompose the whether the properties reflect their intent, while automated verifiers leverage bounded model checking to verify the code. prompt into hierarchical link units. Each unit exposes one Hierarchical documentation display for focused review. implementable behavior or constraint, while preserving its text After translating Python code into documentation (step ➂ in from the original prompt. When a sentence specifies multiple Figure 3) and generating validation questions (step ➃), VLP behaviors, VLP further splits it into smaller clauses. Unlike presents them in a hierarchical view as the user interface. The flat sentence-level linking, this hierarchy lets VLP keep each goal is to avoid making users read the full documentation while link unit concrete while retaining the logical context needed still preserving the surrounding program context needed to to interpret it. This design serves two purposes. First, it helps judge a potential documentation-intent mismatch. Specifically, VLP handle long prompts without collapsing fine-grained documentation lines are grouped into collapsible blocks using requirements into coarse summaries. Instead of asking the function calls and classes as boundaries. For recursive function LLM to produce a single global summary, VLP first identifies calls and class references, the same function or class is coarse implementable behavior regions and then recursively expanded to depth at most two. When a validation question decomposes each region into more detailed child units. The generated in §IV-C highlights a suspicious documentation recursion stops once the relevant text span reaches a manageable snippet, the user interface proactively opens the relevant block size for the LLM to output extracted sentences from the and nearby context. Thus, users only have to review and validate original prompt rather than free-form summaries. Second, the hierarchy preserves logical relations among prompt-side units. a small portion of the documentation. When one unit specifies the condition under which another C. Fine-Grained Intent-Documentation Mismatch Detection behavior should occur, such as an error condition followed by After VLP constructs the documentation, users will validate a required message, the behavior unit is recorded as a child of whether its behavior matches their intent. A full documentation the condition unit. The hierarchy retains the condition/context view is insufficient for complex programming tasks, as users in which each behavior should be implemented.

TABLE II: Fine-grained mismatch detection in VLP. A unit may fall into multiple categories; for example, a line involving both formula logic and API calls is checked under both linked pair with API use and other linked pair. Scope

Mismatch type

LLM check criterion

Validation question

Unlinked prompt unit

Missing steps

A prompt-side unit has no linked documentation unit. The LLM checks whether the behavior is truly required but missing.

Whether the prompt unit should be implemented.

Unlinked doc unit

Redundant steps

A documentation-side unit has no prompt support. The LLM checks whether it is truly redundant behavior or a reasonable enhancement.

Whether the extra program behavior is intended.

Unlinked or ambiguous unit

Prompt underspecification; lacking domain knowledge

The prompt does not fully determine the implementation choice, or the behavior depends on domain-specific conventions.

Corresponding clarification questions.

Linked pair with API use

Wrong action/operation

For python_level blocks that invoke APIs, VLP retrieves API docstrings Which operation or and semantically similar alternatives. The LLM checks whether the current documented API behavior is API behavior matches the intended operation. intended.

Linked pair with API use

Wrong operand/value

The API-level action is correct, but parameters, operands, exception behavior, or boundary cases differ from the prompt.

Other linked pair

Wrong action/operation; Wrong operand/value

The documentation simplifies or misinterprets the required operation. For The intended operation, example, the prompt asks to combine A and B without specifying the operand, or property. formula, while the documentation instantiates it as (A + B)/2.

Function-level flow Wrong execution flow

The prompt-side control-flow sketch and documentation-side execution flow disagree on conditions, loops, or ordering.

The intended details or edge-case behavior.

When or in what order the behavior should occur.

Given the prompt-side and documentation-side candidate units, VLP retrieves the top-k documentation candidates for each prompt unit based on semantic similarity, where k = 3 in our evaluation. Following recent LLM-assisted TLR work [50], an LLM-based judge then confirms or rejects each candidate link using the two units and their surrounding context. Using LLM-assisted TLR allows the recovered links to reflect relevant program behavior rather than superficial textual similarity. Fine-grained misalignment detection. After recovering trace links, VLP uses an LLM to check both linked promptdocumentation pairs and unlinked units for potential mismatches. Guided by the logic-related bug taxonomy in Figure 2, VLP considers seven mismatch types. Table II summarizes the fine-grained detection criteria for each type. We additionally introduce the way to detecting underspecification for linked pairs with API use, which is not illustrated by the table. For a linked pair whose documentation-side unit invokes an API-based python_level block, VLP retrieves the API docstring and top three semantically similar alternatives from an incrementally extended API knowledge base. If the retrieved APIs suggest multiple plausible behaviors or edgecase handling, but the prompt-side unit does not specify which one is intended, VLP treats the case as API-level prompt underspecification and asks the user for clarification.

argument and return-value constraints, and initialization and cleanup. Thus, VLP checks API-level requirements automatically with an LLM in the code repair process. Bounded model checking for properties. During constrained Python generation, VLP emits verifiable properties, including preconditions, postconditions, and invariants, as executable assertions. After users validate these properties in the documentation, VLP checks the corresponding functions with bounded model checking. Concretely, we use CrossHair [51] to symbolically explore program executions and search for inputs that violate the validated assertions. When CrossHair finds a counterexample, VLP feeds the failing input and violated assertion back to the LLM for subsequent program repair.

Our evaluation answers the following research questions: (i) Does VLP generate more correct programs than LLMonly generation and prior human-in-the-loop code generation frameworks (§V-B)? (ii) How accurately does VLP localize intent-documentation mismatches (§V-D)? (iii) How much does VLP affect user satisfaction during repair and validation (§V-D)? (iv) What additional cost does VLP introduce (§V-E)? (v) How much do the API knowledge base and implementationrelevant TLR contribute to VLP’s effectiveness (§V-F)?

D. Automated Verification After User Validation

A. Evaluation Setup

V. E VALUATION

Implementation and evaluated LLMs. We implement VLP Documentation enables users to validate intent-level behavior, but low-level concerns such as Python-specific API require- using LangGraph [52] and NLTK [53]. We evaluate it with ments and the correctness of algorithms are better handled GPT-5.4 [54] and DeepSeek V4 Flash [36] by calling the automatically. To this end, VLP integrates two complementary official APIs with default decoding parameters. verifiers: an API verifier for Python-specific API usage, and Benchmark selection. We evaluate VLP on two complemena bounded model checker for postconditions and invariants tary LLM-for-code benchmarks. (1) We use BigCodeBenchstated in the validated documentation. Instruct [35] (BCB) to evaluate LLM-generated code on Python-specific API verifier. User validation helps ensure tasks with diverse API calls and complex instructions. (2) that the selected APIs match the intended functionality, but We use QuantCodeEval [34] (QCE), a finance paper-to-code users, especially non-programmers, may still be unfamiliar benchmark, to evaluate domain-specific and extremely complex with Python-specific API requirements, such as stateful APIs, code generation tasks.

BCB-21 BCB-254 BCB-344 BCB-389 BCB-493 BCB-597 QCE-T01 QCE-T24 P1 L1 P2 L2 P3 L3 P4 L4

VLP VLP Clari Clari PInG PInG TiCo TiCo

TiCo TiCo VLP VLP Clari Clari PInG PInG

PInG PInG TiCo TiCo VLP VLP Clari Clari

Clari Clari PInG PInG TiCo TiCo VLP VLP

VLP VLP Clari Clari PInG PInG TiCo TiCo

TiCo TiCo VLP VLP Clari Clari PInG PInG

Deepseek V4 Flash

Clari Clari PInG PInG TiCo TiCo VLP VLP

GPT-5.4

Pass@1 (%)

100 80 60 40 20 0

PInG PInG TiCo TiCo VLP VLP Clari Clari

BCB-All

BCB-Hard Default Code

QCE-Full TiCoder

BCB-All ClarifyGPT

BCB-Hard QCE-Full PInG VLP

Fig. 4: Pass@1 on BCB and QCE with user simulation. Metrics. We evaluate VLP from four perspectives: end-toend code correctness, guidance quality, user experience, and cost efficiency. For end-to-end code correctness, we report pass@1 [55] using benchmark-provided tests and property checkers. Pass@1 measures whether a single generated implementation passes all required checks. For guidance quality, we measure the precision of VLP’s mismatch detection (recall is already represented by pass@1), defined as the fraction of suspicious documentation snippets reported by VLP that correspond to ground-truth intent-documentation mismatches. For user experience, we demonstrate code review and validation time and users’ self-reported experience in the user study. Finally, for cost efficiency, we report the average token usage and dollar cost per programming task. Baselines. We compare VLP against four baselines. Default Code directly prompts the LLM to generate code without user review, clarification, or validation. We also compare against three open-source SOTA human-in-the-loop code generation frameworks, covering pre-generation clarification, commentbased validation, and test-driven interaction. ClarifyGPT [24] is a strong pre-generation intent clarification baseline. PInG [40] is a comment-based human-in-the-loop framework that interleaves code generation, comments, and user feedback through editable comments, and is reported to outperform Copilot. We include it to test whether ordinary editable comments are sufficient, or whether VLP’s documentation, guidance, and verifiers provide additional benefits. TiCoder [32] is a testbased intent clarification framework that uses generated tests and user feedback on the tests to infer user intent and refine code. We include it to compare documentation-based validation against test-driven interaction. B. Overall Pass Rate Since our evaluation involves 30 finance papers and 1,140 general programming tasks, conducting the entire evaluation with real users would be prohibitively costly. We therefore

80 60 40 20 00

Passed Checks Over Time 80-check upper bound

Passed checks

TABLE III: Tool and task assignment for users. Clari: ClarifyGPT; TiCo: TiCoder. P/L denote participants with professional and low programming experience, respectively.

User Satisfaction

TiCoder 3.3 2.1 2.4 3.1 3.1 ClarifyGPT 3.7 2.7 2.8 3.1 3.5 PInG 3.4 1.7 4.2 3.6 3.2

15

30

45

Time (min)

TiCoder

GPT + Simulated User + VLP DeepSeek + Simulated User + VLP

ClarifyGPT

PInG

VLP

5 4 3

VLP 4.6 2.4 4.1 4.1 4.0

2

g rt g e n din ffo din nc tio fin ow e stan nfide tisfac L der Co sa ll un era de Ov Co

1

g Bu

Fig. 5: Real user study showing pass@1 over user time (left) and users’ satisfaction (right). The final pass rate of VLP falls between those in the simulated user settings of DeepSeek and GPT. combine real user feedback with an LLM-based user simulator for large-scale evaluation, following prior interactive codegeneration work [24], [32]. The consistency analysis between simulated and real users is in §V-C. LLM-based user simulation. As shown in Table IV, the simulator is provided with oracle context which represents the full vibe coding user intent. The oracle context includes the benchmark prompt and golden reference implementation, so that the user simulator’s feedback is grounded in the intended behavior. This oracle context is available only to the simulator, not to the evaluated framework during code generation or repair. The simulator can only respond to questions posed by VLP, ClarifyGPT, and TiCoder, and update PInG’s comments via their original interaction interface for fair comparison. Moreover, it cannot reveal unrelated code defects proactively. Real user study. We conduct a real-user study on a selected subset to compare VLP with prior human-in-the-loop methods. We recruit 10 participants, reserving 2 for pilot testing to refine task selection, user interfaces, and instructions, and using the remaining 8 in the main study. We sample 8 tasks from the benchmarks, including 2 QCE and 6 BCB tasks that are unsolved by the initial code. Before the study, participants provided informed consent and completed a prestudy questionnaire on their background. For each human-inthe-loop method, we implement a user interface following the paper. The model used in the real-user study is GPT-5.4. We assign tasks and methods to participants according to three criteria, as shown in Table III. First, each selected task is evaluated with all four human-in-the-loop methods, so method comparison is not confounded by task difficulty. Second, each participant sees only one method for the same task, avoiding carryover effects from answering the same task multiple times. Third, each method on each task is assigned to one programmer and one non-programmer participant, reducing confounding from participant expertise. Each participant will respond through the dedicated user interface. Overall pass rate and analysis. Figure 4 and Figure 5 show that VLP consistently improves pass@1 under both LLMsimulated feedback and real user feedback. On BCB, VLP achieves the strongest results for both models, substantially outperforming other baselines. We attribute this advantage

TABLE IV: Method-specific inputs (in addition to the oracle context) and outputs for LLM-based user simulation. Method

Simulator input following the papers

Allowed simulator output

VLP

Validation questions and highlighted documentation (rather than the code).

Answer only the validation questions. The simulator may fix the highlighted statements according to the validation hints, but cannot touch unrelated documentation parts.

ClarifyGPT

Clarification questions generated from the ambiguous requirements [24].

Answer only the asked clarification according to the intended behavior. The simulator cannot provide unsolicited bug fixes or compare the full code with the reference.

PInG

NL comments and the binary PASS/FAIL execution results [40].

Review only the shown comments. The simulator may confirm or edit each comment line, but cannot perform code-level review.

TiCoder

Five candidate tests generated by TiCoder with Return the expected pass/fail outputs of the golden reference code given the input test five candidate code implementations [32]. cases, which follows TiCoder’s open-source Github repository.

TABLE V: Simulator-human consistency. H denotes human- work that validates model-based outputs against human judghuman consistency; S denotes simulator-human consistency. ments [56], [57]. For each task used in both LLM-simulated and real-user settings, we collect all question/comment-feedback Method H-correctness S-correctness H-scope S-scope pairs, anonymize them, and then ask three independent human VLP 0.72 0.69 0.87 0.81 adjudicators to score each response along two dimensions: (i) ClarifyGPT 0.64 0.80 0.96 0.93 PInG 0.87 0.64 1 (all in scope by design) 1 feedback correctness measures whether the response is relevant and accurate with respect to the query or comment line (2: to our fine-grained mismatch detection through the linked correct; 1: relevant but misleading; 0: irrelevant) and (ii) scope documentation and prompts. Moreover, VLP exposes concrete compliance measures whether the response stays within the implementation inconsistencies in the validation questions to queried line (2: no leakage; 1: minor extra detail; 0: excessive users, and therefore eventually results in more actionable cross-scope feedback). repair commands. Nevertheless, VLP still fails on 6.5%– We measure simulator-human consistency on each rubric 33.8% of BCB tasks. Besides LLM inherent randomness, the dimension d ∈ {correctness, scope}, corresponding to feedback remaining BCB failures are often caused by totally unstated correctness and scope compliance. Let N be the number operations that the prompts never mention. For example, in of questions/comments generated by GPT-5.4, and let each BCB-306, the prompt asks to remove all JavaScript files question/comment have one simulator response and J real-user whose names contain jquery and record the removed files responses. For question/comment i, we denote the simulator in jquery_removal.log; it never specifies that the im- response as s and the j-th real-user response as h . For each i ij plementation should use Python’s logging module or call response, we aggregate scores from independent adjudicators logging.info. Nevertheless, the BCB checker expects such by majority vote, using the median score to break ties; r̂ (x) d a call, making this hidden requirement difficult for VLP denotes the resulting adjudicated score of response x on to detect. Other failures arise when the correct feedback is dimension d. We then compare the simulator score with the not correctly applied by the repair LLM since it requires average human score: PJ coordinated edits across scattered code snippets. N r̂d (si ) − J1 j=1 r̂d (hij ) X 1 On QCE, VLP also improves the code generated by S IM C ONSd = 1 − . N i=1 2 both models, especially for DeepSeek. However, it does not We also report average leave-one-out human-human consisachieve full correctness because QCE tasks require substantial quantitative finance knowledge, such as reasoning about time- tency for reference. The overall results in Table V show that window alignment and look-ahead bias. VLP is not designed simulator feedback is reasonably aligned with human feedback. to detect inconsistencies beyond the LLM’s knowledge and Scope compliance is a bit less consistent for VLP, because prompt. Furthermore, even when such inconsistencies are fixing a bug may go beyond the scope of the documentation identified and the user provides the correct feedback, the line directly associated with the question/comment. repair model may still fail to implement the required changes, D. Quality of Validation Questions from VLP especially for DeepSeek. Overall, these results suggest that In this section, we evaluate user validation burden and VLP is most effective when missing requirements or semantic deviations can be grounded in the program or prompt, while question usefulness. On BCB, VLP asks 8.79 questions per its remaining limitations stem primarily from the underlying task on average with GPT-5.4 and 2.87 with DeepSeek V4 Flash, corresponding to 0.223 and 0.098 questions per line of model’s domain knowledge and code repair capability. code. On QCE, it asks 86.07 and 11.63 questions per task, C. Simulated vs. Real User Consistency Analysis with corresponding question-to-code-line ratios of 0.264 and Because simulator feedback affects the final pass@1, we 0.053. Among these questions, after review, 55.1% and 64.1% examine whether it approximates real human feedback. Note of cases on QCE and BCB require code modifications for that TiCoder is excluded because users only need to accept DeepSeek, respectively, compared with 55.2% and 66.3% for or reject test cases without any NL interaction. We use blind GPT. Since GPT poses more questions, with a code-correcting rubric-based adjudication, which is inspired by LLM-as-a-judge question rate similar to DeepSeek, the simulated user plus GPT

Tokens (K)

1000 750 500 250 40 30 20 10 0

Deepseek V4 Flash

GPT-5.4

the two ablations both reduce pass@1 from 66.2% to 58.8%. These drops show that both components are important. G. Limitations and Threats to Validity

First, although LLMs may have been trained on opensource dataset, data leakage is unlikely to substantially affect our results because VLP validates and repairs errors that Default Code TiCoder ClarifyGPT PInG VLP Input Output remain in LLM-generated programs rather than reproducing Fig. 6: Average tokens spent on BCB and QCE. benchmark solutions. Moreover, QuantCodeEval [34], released in May 2026, is unlikely to have appeared in model training can cover more intent mismatches. Compared with ClarifyGPT data. Second, due to the cost of large-scale user studies, we (0.015-0.164 questions per line) and PInG, VLP generally combine a real-user study with an LLM-based user simulator. achieves a higher review-trigger rate than ClarifyGPT while We improve simulation fidelity with clarifying questions and eliciting substantially more user feedback, yet it requires far ground-truth test cases, and observe close agreement between less review effort than PInG’s line-by-line comment review. simulated and real-user feedback (§V-C). Finally, we do Finally, question quality varies across LLMs used for detection, not evaluate the faithfulness of the documentation separately suggesting that the misalignment-detection prompt may require because most of it is enforced by a deterministic, syntaxmodel-specific calibration. directed translation. For API calls that require LLM-assisted After finishing a programming task, the participant answered translation, the LLM is provided with API documentation 5 survey questions for the used method, with scores ranging and constrained by our syntax, while the exact control flow, from 1 (low) to 5 (high). The questions measure helpfulness arguments, return targets, and data dependencies are preserved. for finding code issues, low labor intensity, understanding of the generated code, confidence in using the code beyond VI. R ELATED W ORK simple tests, and overall satisfaction. Higher scores indicate Validating/verifying LLM-generated code. Existing apbetter user experience for all metrics. Figure 5 shows that VLP achieves the highest scores in helpfulness for mismatch proaches to validating/verifying LLM-generated code mainly detection, code understanding, and confidence in using the fall into two groups. The first detects likely errors using code, while maintaining a lower labor-intensity than PInG and probabilistic methods, such as LLM-generated tests [7], [9], TiCoder. These results suggest that guided validation over code- LLM judges, task-specific rules, risk prediction based on LLM derived documentation helps users validate LLM-generated internal states, calibration, or metamorphic testing [58]–[61]. They can reveal failures, but cannot guarantee correctness. code with a better balance between correctness and effort. The second group uses certificate-based verification, where generated code or specifications are checked by formal tools. E. Token and User Time Cost These methods rely on expert-written or LLM-generated Figure 6 and Figure 5 show the token cost and user pass@1 properties [19], [62]–[68], verifier-guided refinement [13], over time of each method, respectively. On BCB, VLP uses or runtime checks with expert knowledge [69]. Their key 27.3K tokens per task on average with GPT-5.4 and 32.1K bottleneck is certificate quality: current LLMs often fail to with DeepSeek V4 Flash; on QCE, it uses 291.1K and 337.2K produce properties that are both verifiable and complete enough tokens, respectively. When we use DeepSeek and VLP to to exclude incorrect behaviors [18], [70], [71]. approach GPT’s performance on complex tasks such as QCE, Human-in-the-loop for vibe coding. Human-in-the-loop although 7.66× more tokens are used, the cost efficiency is techniques have been explored to make AI-assisted prostill 2.33×–6.99× higher. In the real-user study, VLP slows gramming more controllable. Prior work studies developer users down more noticeably on short coding tasks, especially interactions with coding assistants [72]–[74], elicits intent when using GPT, which asks more questions. However, for through intermediate feedback [75], and updates generated code some more complex BCB and all QCE tasks used in real user using runtime feedback or interactive model decisions [76]–[78]. study, where the code is longer, VLP almost lies on the Pareto However, these systems mostly expose code snippets, tests, or frontier when considering both pass rate and user response runtime results to users. VLP instead asks users to validate time. It achieves higher correctness than faster methods and a human-readable NL representation of program semantics lower user time than methods with comparable correctness. before verifying the code implementation. Ambiguous or contradictory prompts can substantially F. Ablation Study degrade code correctness even when models still generate We conduct an ablation study on BCB-Hard to measure the plausible code [79]. Existing work reduces underspecification contribution of the API knowledge base and implementation- mainly through pre-generation clarification or specificationrelevant TLR. With GPT-5.4, removing the API knowledge oriented prompting [24], [27], [32], [80]. In contrast, VLP base decreases pass@1 from 91.9% to 85.1%, while removing traces fine-grained links between the prompt and generated TLR decreases pass@1 to 72.3%. With DeepSeek V4 Flash, code, enabling iterative discovery of subtle mismatches. BCB-All BCB-Hard QCE-Full

BCB-All BCB-Hard QCE-Full

VII. C ONCLUSION We present VLP, a human-in-the-loop framework that introduces an unambiguous literate documentation layer to bridge prompts and LLM-generated code. By enabling fine-grained misalignment detection, targeted user feedback, and automated verification over user-validated semantics, VLP improves code correctness with user validation effort, demonstrating that structured and user-friendly human-LLM collaboration is more effective than purely automated validation. R EFERENCES [1] Anthropic, “2026 agentic coding trends report,” https: //resources.anthropic.com/hubfs/2026%20Agentic%20Coding% 20Trends%20Report.pdf?hsLang=en, 2026. [2] Li, Matt, “Top vibe coding statistics & trends,” https://www.secondtalent. com/resources/vibe-coding-statistics/, 2026. [3] Y.-H. Chou, B. Jiang, Y. W. Chen, M. Weng, V. Jackson, T. Zimmermann, and J. A. Jones, “Building software by rolling the dice: A qualitative study of vibe coding,” arXiv preprint arXiv:2512.22418, 2025. [4] A. Fawzy, A. Tahir, and K. Blincoe, “Vibe coding in practice: Motivations, challenges, and a future outlook–a grey literature review,” arXiv preprint arXiv:2510.00328, 2025. [5] S. K. Lahiri, “Intent formalization: A grand challenge for reliable coding in the age of ai agents,” arXiv preprint arXiv:2603.17150, 2026. [6] Sonar, “State of code developer survey report,” https://www.sonarsource. com/state-of-code-developer-survey-report.pdf, 2026. [7] A. Ni, S. Iyer, D. Radev, V. Stoyanov, W.-t. Yih, S. Wang, and X. V. Lin, “Lever: Learning to verify language-to-code generation with execution,” in International Conference on Machine Learning. PMLR, 2023, pp. 26 106–26 128. [8] N. Alshahwan, J. Chheda, A. Finogenova, B. Gokkaya, M. Harman, I. Harper, A. Marginean, S. Sengupta, and E. Wang, “Automated unit test improvement using large language models at meta,” in Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024, pp. 185–196. [9] Z. Ma, T. Zhang, Maosongcao, J. Liu, W. Zhang, M. Luo, S. Zhang, and K. Chen, “Rethinking verification for LLM code generation: From generation to testing,” in The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. [Online]. Available: https://openreview.net/forum?id=Gp2vgxWROE [10] W. Wang, C. Yang, Z. Wang, Y. Huang, Z. Chu, D. Song, L. Zhang, A. R. Chen, and L. Ma, “Testeval: Benchmarking large language models for test case generation,” in Findings of the Association for Computational Linguistics: NAACL 2025, 2025, pp. 3547–3562. [11] B. R. Korraprolu, P. Pinninti, and Y. R. Reddy, “Test case generation for requirements in natural language-an llm comparison study,” in Proceedings of the 18th Innovations in Software Engineering Conference, 2025, pp. 1–5. [12] N. S. Mathews and M. Nagappan, “Test-driven development and llm-based code generation,” in Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, 2024, pp. 1583–1594. [13] Y. Cai, Z. Hou, D. Sanán, X. Luan, Y. Lin, J. Sun, and J. S. Dong, “Automated program refinement: Guide and verify code large language model with refinement calculus,” Proceedings of the ACM on Programming Languages, vol. 9, no. POPL, pp. 2057–2089, 2025. [14] H. Wu, C. Barrett, and N. Narodytska, “Lemur: Integrating large language models in automated program verification,” arXiv preprint arXiv:2310.04870, 2023. [15] C. Sun, Y. Sheng, O. Padon, and C. Barrett, “Clover: Clo sed-loop ver ifiable code generation,” in International Symposium on AI Verification. Springer, 2024, pp. 134–155. [16] M. Sevenhuijsen, K. Etemadi, and M. Nyberg, “Vecogen: Automating generation of formally verified c code with large language models,” in 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE). IEEE, 2025, pp. 101–112. [17] A. Councilman, D. J. Fu, A. Gupta, C. Wang, D. Grove, Y.-X. Wang, and V. Adve, “Towards formal verification of llm-generated code from natural language prompts,” arXiv preprint arXiv:2507.13290, 2025.

[18] Y. Wang, J. Zhou, H. Lyu, Z. Chao, T. Wang, and H. Li, “Deepassert: An llm-aided verification framework with fine-grained assertion generation for modules with extracted module specifications,” arXiv preprint arXiv:2509.14668, 2025. [19] C. Barrett, T. A. Henzinger, and S. A. Seshia, “Certificates in ai: Learn but verify,” Commun. ACM, vol. 69, no. 1, p. 66–75, Dec. 2025. [Online]. Available: https://doi.org/10.1145/3737447 [20] G. Ryan, S. Jain, M. Shang, S. Wang, X. Ma, M. K. Ramanathan, and B. Ray, “Code-aware prompting: A study of coverage-guided test generation in regression setting using llm,” Proceedings of the ACM on Software Engineering, vol. 1, no. FSE, pp. 951–971, 2024. [21] J. Altmayer Pizzorno and E. D. Berger, “Coverup: Effective high coverage test generation for python,” Proceedings of the ACM on Software Engineering, vol. 2, no. FSE, pp. 2897–2919, 2025. [22] S. Gu, N. Nashid, and A. Mesbah, “Llm test generation via iterative hybrid program analysis,” arXiv preprint arXiv:2503.13580, 2025. [23] G. Crupi, R. Tufano, A. Velasco, A. Mastropaolo, D. Poshyvanyk, and G. Bavota, “On the effectiveness of llm-as-a-judge for code generation and summarization,” IEEE Transactions on Software Engineering, 2025. [24] F. Mu, L. Shi, S. Wang, Z. Yu, B. Zhang, C. Wang, S. Liu, and Q. Wang, “Clarifygpt: A framework for enhancing llm-based code generation via requirements clarification,” Proceedings of the ACM on Software Engineering, vol. 1, no. FSE, pp. 2332–2354, 2024. [25] H.-S. X. Li, M. Mesgar, A. F. Martins, and I. Gurevych, “Python code generation by asking clarification questions,” in Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 2023, pp. 14 287–14 306. [26] H. Darji and T. Lutellier, “Curiosity by design: An llm-based coding assistant asking clarification questions,” arXiv preprint arXiv:2507.21285, 2025. [27] C. Miao, Y. Wang, L. He, L. Fang, and P. S. Yu, “Clarigen: Bridging instruction gaps via interactive clarification in code generation,” in AAAI 2025 Workshop on Preventing and Detecting LLM Misinformation (PDLM), 2025. [28] J. J. Wu, “Large language models should ask clarifying questions to increase confidence in generated code,” arXiv preprint arXiv:2308.13507, 2023. [29] H. Jia, R. Morris, H. Ye, F. Sarro, and S. Mechtaev, “Automated repair of ambiguous problem descriptions for llm-based code generation,” arXiv preprint arXiv:2505.07270, 2025. [30] J. Dong, J. Sun, W. Zhang, J. S. Dong, and D. Hao, “Contested: Consistency-aided tested code generation with llm,” Proceedings of the ACM on Software Engineering, vol. 2, no. ISSTA, pp. 596–617, 2025. [31] E. Firouzi and M. Ghafari, “Persistent human feedback, llms, and static analyzers for secure code generation and vulnerability detection,” arXiv preprint arXiv:2602.05868, 2026. [32] S. Fakhoury, A. Naik, G. Sakkas, S. Chakraborty, and S. K. Lahiri, “Llmbased test-driven interactive code generation: User study and empirical evaluation,” IEEE Transactions on Software Engineering, vol. 50, no. 9, pp. 2254–2268, 2024. [33] J. M. Zhang, M. Harman, L. Ma, and Y. Liu, “Machine learning testing: Survey, landscapes and horizons,” IEEE Transactions on Software Engineering, vol. 48, no. 1, pp. 1–36, 2020. [34] W. Lu, Z. Yuan, H. Wu, D. Jin, and C. Wu, “Quantcode-eval: Benchmarking quantitative strategy code reproduction from finance papers,” Available at SSRN 6801618, 2026. [35] T. Y. Zhuo, M. C. Vu, J. Chim, H. Hu, W. Yu, R. Widyasari, I. N. B. Yusuf, H. Zhan, J. He, I. Paul et al., “Bigcodebench: Benchmarking code generation with diverse function calls and complex instructions,” arXiv preprint arXiv:2406.15877, 2024. [36] DeepSeek-AI, “Deepseek v4 flash,” https://www.deepseek.com, 2026. [37] Anthropic, “Claude opus 4.7,” https://www.anthropic.com/claude/opus, 2026. [38] D. E. Knuth, “Literate programming,” The computer journal, vol. 27, no. 2, pp. 97–111, 1984. [39] K. Shi, D. Altınbüken, S. Anand, M. Christodorescu, K. Grünwedel, A. Koenings, S. Naidu, A. Pathak, M. Rasi, F. Ribeiro et al., “Natural language outlines for code: Literate programming in the llm era,” in Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering, 2025, pp. 150–161. [40] Y. Di and T. Zhang, “Enhancing code generation via bidirectional comment-level mutual grounding,” arXiv preprint arXiv:2505.07768, 2025.

[41] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, “Bounded model checking.” Handbook of satisfiability, vol. 185, no. 99, pp. 457– 481, 2009. [42] Jupyter, “Jupyter notebook: The classic notebook interface,” https:// jupyter.org/, 2026. [43] E. M. Clarke, “Model checking,” in International conference on foundations of software technology and theoretical computer science. Springer, 1997, pp. 54–56. [44] V. R. Pratt, “Semantical considerations on floyd-hoare logic,” in 17th Annual Symposium on Foundations of Computer Science (sfcs 1976). IEEE, 1976, pp. 109–121. [45] A. W. Biermann and B. W. Ballard, “Toward natural language computation i,” American Journal of Computational Linguistics, vol. 6, no. 2, pp. 71–86, 1980. [46] L. A. Miller, “Natural language programming: Styles, strategies, and contrasts,” IBM Systems Journal, vol. 20, no. 2, pp. 184–215, 1981. [47] C. Peng, M. Jiang, Y. Zhou, and L. Wu, “Thought is all you need: Smart contract vulnerability detection with thought-augmented large language model,” Proc. ACM Softw. Eng., vol. 3, no. FSE, 2026. [Online]. Available: https://doi.org/10.1145/3808141 [48] D. Zhou, N. Schärli, L. Hou, J. Wei, N. Scales, X. Wang, D. Schuurmans, C. Cui, O. Bousquet, Q. Le et al., “Least-to-most prompting enables complex reasoning in large language models,” arXiv preprint arXiv:2205.10625, 2022. [49] G. Antoniol, G. Canfora, G. Casazza, A. De Lucia, and E. Merlo, “Recovering traceability links between code and documentation,” IEEE transactions on software engineering, vol. 28, no. 10, pp. 970–983, 2002. [50] D. Fuchβ, T. Hey, J. Keim, H. Liu, N. Ewald, T. Thirolf, and A. Koziolek, “Lissa: Toward generic traceability link recovery through retrieval-augmented generation,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 1396– 1408. [51] W. Wang, K. Liu, A. R. Chen, G. Li, Z. Jin, G. Huang, and L. Ma, “Python symbolic execution with llm-powered code generation,” arXiv preprint arXiv:2409.09271, 2024. [52] H. Chase, “Langchain,” https://github.com/langchain-ai/langchain, 2022. [53] S. Bird, E. Klein, and E. Loper, Natural language processing with Python: analyzing text with the natural language toolkit. " O’Reilly Media, Inc.", 2009. [54] A. Singh, A. Fry, A. Perelman, A. Tart, A. Ganesh, A. El-Kishky, A. McLaughlin, A. Low, A. Ostrow, A. Ananthram et al., “Openai gpt-5 system card,” arXiv preprint arXiv:2601.03267, 2025. [55] M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. D. O. Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman et al., “Evaluating large language models trained on code,” arXiv preprint arXiv:2107.03374, 2021. [56] L. Zheng, W.-L. Chiang, Y. Sheng, S. Zhuang, Z. Wu, Y. Zhuang, Z. Lin, Z. Li, D. Li, E. Xing et al., “Judging llm-as-a-judge with mt-bench and chatbot arena,” Advances in neural information processing systems, vol. 36, pp. 46 595–46 623, 2023. [57] S. Kim, J. Shin, J. Jang, S. Longpre, H. Lee, S. Yun, R. Shin, S. Kim, J. Thorne, M. Seo et al., “Prometheus: Inducing fine-grained evaluation capability in language models,” in International Conference on Learning Representations, vol. 2024, 2024, pp. 29 927–29 962. [58] Y. Fang, B. Chen, J. Peng, X. Li, Y. Xi, C. Zhang, and G. Zhong, “Fewer hallucinations, more verification: A three-stage llm-based framework for asr error correction,” arXiv preprint arXiv:2505.24347, 2025. [59] G. Sriramanan, S. Bharti, V. S. Sadasivan, S. Saha, P. Kattakinda, and S. Feizi, “Llm-check: Investigating detection of hallucinations in large language models,” Advances in Neural Information Processing Systems, vol. 37, pp. 34 188–34 216, 2024. [60] C. Spiess, D. Gros, K. S. Pai, M. Pradel, M. R. I. Rabin, A. Alipour, S. Jha, P. Devanbu, and T. Ahmed, “Calibration and correctness of language models for code,” in 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE). IEEE, 2025, pp. 540–552. [61] X. Wang and D. Zhu, “Validating llm-generated programs with metamorphic prompt testing,” arXiv preprint arXiv:2406.06864, 2024. [62] L. He, Z. Chen, Z. Zhang, J. Shao, X. Gao, and L. Sheng, “Use propertybased testing to bridge llm code generation and validation,” arXiv preprint arXiv:2506.18315, 2025. [63] E. Meijer, “Guardians of the agents,” Commun. ACM, vol. 69, no. 1, p. 46–52, Dec. 2025. [Online]. Available: https://doi.org/10.1145/3777544

[64] Q. Liu, M. Zou, H. Zhang, D. Du, Y. Xia, and H. Chen, “Sharpen the spec, cut the code: A case for generative file system with sysspec,” arXiv preprint arXiv:2512.13047, 2025. [65] H. Ding, Z. Wang, and H. Chen, “Fm-agent: Scaling formal methods to large systems via llm-based hoare-style reasoning,” arXiv preprint arXiv:2604.11556, 2026. [66] Z. Xu, X. Cheng, J. Xue, and Y. Li, “Self-spec: Model-authored specifications for reliable llm code generation,” in Open Conference of AI Agents for Science 2025. [67] D. Delimarsky and M. Riem, “Spec Kit,” Apr. 2026. [Online]. Available: https://github.com/github/spec-kit [68] Y. Liu, Y. Xue, D. Wu, Y. Sun, Y. Li, M. Shi, and Y. Liu, “Propertygpt: Llm-driven formal verification of smart contracts through retrievalaugmented property generation,” arXiv preprint arXiv:2405.02580, 2024. [69] Y. Zhang, S. Y. Emma, A. L. J. En, and J. S. Dong, “RvLLM: LLM runtime verification with domain knowledge,” in The Thirty-ninth Annual Conference on Neural Information Processing Systems, 2025. [Online]. Available: https://openreview.net/forum?id=XdwPWKbxd9 [70] M. Rego, W. Fan, X. Hu, S. Dod, Z. Ni, D. Xie, J. DiVincenzo, and L. Tan, “Evaluating the ability of gpt-4o to generate verifiable specifications in verifast,” in 2025 IEEE/ACM Second International Conference on AI Foundation Models and Software Engineering (Forge). IEEE, 2025, pp. 246–251. [71] M. Hassan, S. Ahmadi-Pour, K. Qayyum, C. K. Jha, and R. Drechsler, “Llm-guided formal verification coupled with mutation testing,” in 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 2024, pp. 1–2. [72] S. Barke, M. B. James, and N. Polikarpova, “Grounded copilot: How programmers interact with code-generating models,” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, pp. 85–111, 2023. [73] H. Mozannar, G. Bansal, A. Fourney, and E. Horvitz, “Reading between the lines: Modeling user behavior and costs in ai-assisted programming,” in Proceedings of the 2024 CHI conference on human factors in computing systems, 2024, pp. 1–16. [74] P. Vaithilingam, E. L. Glassman, P. Groenwegen, S. Gulwani, A. Z. Henley, R. Malpani, D. Pugh, A. Radhakrishna, G. Soares, J. Wang et al., “Towards more effective ai-assisted programming: A systematic design exploration to improve visual studio intellicode’s user experience,” in 2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP). IEEE, 2023, pp. 185– 195. [75] C. Zhu-Tian, Z. Xiong, X. Yao, and E. Glassman, “Sketch then generate: Providing incremental user feedback and guiding llm code generation through language-oriented code sketches,” arXiv preprint arXiv:2405.03998, 2024. [76] K. Ferdowsi, R. Huang, M. B. James, N. Polikarpova, and S. Lerner, “Validating ai-generated code with live programming,” in Proceedings of the 2024 CHI conference on human factors in computing systems, 2024, pp. 1–8. [77] E. A. González, R. Rothkopf, S. Lerner, and N. Polikarpova, “Hilde: Intentional code generation via human-in-the-loop decoding,” in 2025 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC). IEEE, 2025, pp. 222–233. [78] W. Takerngsaksiri, J. Pasuksmit, P. Thongtanunam, C. Tantithamthavorn, R. Zhang, F. Jiang, J. Li, E. Cook, K. Chen, and M. Wu, “Human-in-theloop software development agents,” in 2025 IEEE/ACM 47th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP). IEEE, 2025, pp. 342–352. [79] M. Larbi, A. Akli, M. Papadakis, R. Bouyousfi, M. Cordy, F. Sarro, and Y. L. Traon, “When prompts go wrong: Evaluating code model robustness to ambiguous, contradictory, and incomplete task descriptions,” arXiv preprint arXiv:2507.20439, 2025. [80] C. Yang, Y. Shi, Q. Ma, M. X. Liu, C. Kästner, and T. Wu, “What prompts don’t say: Understanding and managing underspecification in llm prompts,” arXiv preprint arXiv:2505.13360, 2025.