arXiv CSopen access

AfterVibe: What Remains When the Conversation Ends

AfterVibe: What Remains When the Conversation Ends Matteo Paltenghi , Satish Chandra

arXiv:2607.09900v1 [cs.SE] 10 Jul 2026

Meta, USA We present AfterVibe, a framework that recovers natural-language specifications from a vibe coding session. Given a code artifact and the conversation trajectory that produced it, AfterVibe uses an LLM to extract an abstract natural-language specification capturing the developer’s intent, and validates it through a regeneration test: a second, blind AI agent re-implements the artifact from the spec alone, and the resulting code is graded against the original through a multi-tier validation pipeline. Spec quality is thus measured by whether an agent can regenerate passing code; if the verifiers deem the implementations equivalent the spec is considered strong, otherwise it is iteratively refined. Evaluating AfterVibe on 72 real-world vibe-coded projects from a company’s internal coding sessions, we find that its recovered specs are abstract by design—capturing behavioral intent without dictating implementation—yet strong. Multiple independent regenerations achieve a high mean regeneration score of 5.06 out of 6.0 while remaining diverse in their details, confirming that the spec constrains what without over-prescribing how. Besides outperforming existing human-authored descriptions, the specs can be further strengthened iteratively to a score of 5.74. A practical implication is that specifications—not code—could become the primary artifact for human review and the source of record at a time when AI-generated code is outpacing customary code review. Correspondence: Matteo Paltenghi ([email protected]), Satish Chandra ([email protected])

1

Introduction

The advent of powerful large language models (LLMs) and coding agents has enabled a new style of programming in which developers describe what they want in natural language and let an AI assistant generate the code. Andrej Karpathy coined the term vibe coding 1 to describe this practice: “you fully give in to the vibes, embrace exponentials, and forget that the code even exists.” What was once a niche experiment has rapidly become mainstream—millions of developers now use AI coding assistants daily, and entire startups ship products built almost exclusively through conversational prompting. In this work, we use “vibe coding” broadly to denote any code change produced through conversational interaction with an AI coding agent—including production-quality changes at scale that are ultimately reviewed and landed as accepted pull requests. A well-known problem with vibe coding is no one fully understands the code—not even the developer who prompted it into existence. Traditional software engineering relies on the assumption that someone—be it the original author or a reviewer—can read, reason about, and vouch for the correctness of source code. Vibe coding undermines this assumption at its root. The developer’s intent lives ephemerally in a chat transcript; the generated code is voluminous and often opaque; and the mapping between the two is implicit at best. This situation is especially problematic for code review, one of the most important quality-assurance practices in modern software engineering (Bacchelli and Bird, 2013). A reviewer confronted with ever-growing volume of AI-generated code has no concise, authoritative document that states what the code is supposed to do. The result is that a growing class of software that is effectively unreviewable, and not just because of the rate of code production. A recent industry study (DORA, 2025) finds code review not keeping up with AI-based code production. We propose AfterVibe, a framework that bridges the gap between vibe coding and traditional quality assurance. The name reflects its purpose: it captures what remains after a vibe coding session ends—a 1 Andrej Karpathy, There’s a New Kind of Coding Emerging, X/Twitter post, February 2025.

1

durable natural language specification distilled from the ephemeral conversation. AfterVibe takes as input a code artifact and the conversation trajectory that produced it, and outputs a structured specification—what we call a spec. The spec captures the developer’s intent in natural language; crucially, we treat requirements as implicit—whatever is observable from the session is a sufficient expression of the requirements, since the developer’s actions during the session serve as a proxy for their mental model. To validate the faithfulness of the extracted specification, AfterVibe employs a new regeneration test: a second, independent AI agent attempts to rebuild the artifact from the spec alone. The regenerated code is then compared against the original artifact through a three-tier verification pipeline: (1) flexible test execution using tests extracted from the session, (2) verification conditions (VCs) extracted independently from the conversation trajectory, and (3) ground-truth alignment checking via structured LLM reasoning (Ugare and Chandra, 2026). If the verifier deems the implementations equivalent, the spec is considered faithful; if not, the process iterates. The regeneration test recalls the classical principle of design diversity and N-version programming (Chen and Avizienis, 1978; Knight and Leveson, 1986): independent re-implementations of the same intent expose ambiguity and unstated assumptions in a specification. Our results show that natural-language specs derived from vibe coding sessions are essentially sufficient to reconstruct the original code, are abstract, and can be obtained as a byproduct of the vibe coding process rather than requiring separate authoring effort. Recovering requirements after implementation is the long-standing aim of requirements traceability (Gotel and Finkelstein, 1994); AfterVibe is the first to pursue it directly from human-AI coding trajectories. Contributions. This paper makes the following contributions:

⋆ Retrospective specification recovery. We introduce retrospective specification recovery, the first technique to reconstruct developer intent after coding, directly from the agent trajectory (the conversation and code diff) of an AI-assisted coding session. ⋆ The regeneration strength test. We propose the regeneration test, an oracle that deems a specification faithful when a blind agent can regenerate functionally equivalent code from it alone, scored by a three-tier agent-as-a-judge verifier. ⋆ Evidence of real-world effectiveness. We implement the technique in AfterVibe and evaluate it on 72 real-world, vibe-coded tasks from an industrial monorepo where recovered specifications reach a mean regeneration score of 5.74/6.0 after iterative strengthening. ⋆ Specs that are abstract yet sufficient. We show that recovered specifications are abstract by design— independent regenerations succeed while differing substantially in implementation, so a spec constrains what without over-prescribing how. The specs are also significantly more concise than the diff in size: average reduction of 5.6x in chars. Vision. Our vision is that specifications, not code, should be the primary artifact of human authorship in the

age of AI-assisted development. Code—whether written by a human or generated by an AI—is merely an implementation of intent. By elevating specifications to first-class status, we enable a new review paradigm in which humans inspect abstract, readable statements of intent rather than voluminous, machine-generated code. Beyond review, the specification can serve as the source of record —the canonical artifact from which an implementation can be reconstructed, analogously to how executable code is compiled from high-level languages. This paper has shown the feasibility of recovering specifications from vibe coding sessions automatically. In future work, we plan to study empirically whether and how well such specifications can get adopted as the artifact to be reviewed and possibly a trusted source of record.

2

Motivating Example

To ground the discussion, we walk through an example inspired by a real internal coding session (anonymized). A developer rewrites a resource-cleanup utility: a component that, when a logical tenant is torn down, deletes the tenant’s leftover bookkeeping records across several internal stores. The original implementation was blind —it issued a delete for every record type in every group whether or not the record existed—wasting a rate-limited write budget. The developer uses an AI coding assistant to refactor it into a scan-then-delete 2

Part A: Specification Intent and Rationale. “This change refactors the [[cleanup-utility class]] from a shard-group-centric cleanup model into a type-centric, scan-then-delete cleanup model. [...] each cleanup helper now scans its own group first and only deletes entities that actually exist.” Essential Design Decisions. (original 12 items; shown 1) “Each per-type group helper must scan its group once before deleting, so only existing entities consume the rate-limited write budget. [...] read failures must not inflate FOUND or DELETED_FAILED but must flip success and surface a message.” Undiscoverable Facts. (original 12 items; shown 2)

• “The external-operations tri-state codes are: 0 = not present, 1 = deleted or dry-run, 2 = delete failed, 3 = read failed.” • “The [[placement service]] is not governed by [[write rate-limiter]]; this is why its fan-out must be explicitly bounded.” Part B: Requirements (2 of 34 shown)

• The external-operations cleanup distinguishes read failures (code 3) from delete failures (code 2), and read failures do not increment FOUND or DELETED_FAILED. • The [[placement service]] delete fan-out uses windowed concurrency bounded by the inner parallelism flag, not an unbounded [[unbounded-collect helper]]. Figure 1 Full AfterVibe post-hoc spec (Part A + Part B).

Title. [[project tag]] Make [[cleanup-utility class]] scan-then-delete per type with per-group summary. Summary. [[cleanup tool]] now scans each entity type once per group and deletes only entities that exist, replacing the old shard-group-by-shard-group walk. Motivation: the old approach spent the rate-limited write budget on no-op deletes, and an unbounded [[placement service]] fan-out flooded the store with not-found errors. [...] Test plan. Built the targets; ran the unit tests (Pass 7 / 9 / 8); lint clean; manually deleted all consolidated tiers. Figure 2 Full human-authored summary.

model and to fix a cluster of correctness and robustness issues. The resulting change spans over 100,000 characters across many files. AfterVibe takes the change and the conversation transcript as input and produces the structured specification of Fig. 1.2 The full AfterVibe spec is under 10,000 characters. The full post-hoc specification (Fig. 1) has two parts—Part A: Specification (three prose sections) and Part B: Requirements (a behavioral checklist of declarative statements)—which together we refer to as the spec, and which are what a blind agent regenerates from. For contrast, the developer’s own review description—title, summary, and test plan—used verbatim as a baseline “spec” (Fig. 2, shortened). Both artifacts describe the same change, and the human summary is not vague—it names the scan-then-delete idea, the typed result, and the bounded fan-out. Yet the two rebuilds diverge sharply. The AfterVibe rebuild passes both extracted tests (2/2), satisfies all twelve verification conditions (12/12), and matches the reference on a holistic review, for a perfect 6 out of 6; the summary’s rebuild passes neither test (0/2), meets only three of the twelve verification conditions (3/12), and fails the holistic review, scoring 0.5. The reason is that a changelog reports what happened whereas a re-implementer needs the exact rules to follow. Two of the verification conditions—shown in Fig. 3—make this concrete. For each, our spec states the exact rule (the distinct codes returned for a failed read versus a failed delete, and that a tenant is skipped only when both group lists are empty), so the rebuilt code satisfies the check. The summary omits both distinctions, so its rebuild merges the two failure cases and stops as soon as either list is empty, failing both checks. The same gap breaks the build itself: our spec names the exact build dependency to switch, whereas the summary only 2 In the excerpts, [...] marks elided text and names in double-bracketed typewriter font (e.g. [[cleanup-utility class]]) are anonymized placeholders for real internal identifiers. Technical values (return codes, field keys, defaults) are non-identifying and kept verbatim.

3

Verification conditions.

• Is a failed read of a record counted separately from a failed delete, and never tallied as a delete failure? • Does the cleanup skip a tenant only when both of its two group lists are empty, still cleaning the other when only one is empty? Figure 3 Verification conditions: checks the grader extracts independently of the spec and runs on both the original

and the rebuilt code (2 of 12 shown).

refine if weak

1

Traj. T

Requirements (implicit)

Vibe-coding session

Code C

Blind Agent

Spec S

VC Extraction

Verif. Cond.

VC Check (×2)

checked to pass on Code C ✓

Flex Test (×3)

2

Metadata M

Regeneration Test

4

only input

Spec Distillation

Code C ′

Three-Tier Verifier

3

Test Command Extraction

Test Commands

5

+

regen score (0–6)

GT Align (×1)

checked to pass on Code C ✓

Figure 4 Overview of the AfterVibe workflow. From a vibe-coding session (trajectory T , summary M , code C), AfterVibe ➀ distills a specification S; ➁ extracts verification conditions and ➂ test commands (both validated on C as oracles); ➃ regenerates code C ′ from S alone with a blind agent; and ➄ scores it with a three-tier verifier, iteratively refining S when the score is weak.

says the data now comes from a different source, so the rebuilt project files disagree with the code and it never compiles—which is why neither of its tests can run.

3

Approach

Figure 4 gives an overview of the AfterVibe workflow: from a vibe-coding session it distills a specification, derives oracles (verification conditions and test commands), regenerates code from the specification alone, and scores the regeneration with a three-tier verifier, iteratively refining the specification when the score is weak. We detail each stage in the remainder of this section.

3.1

Problem Formulation

We define the retrospective specification recovery problem as follows. Given a code change C (unified diff) produced by an AI coding assistant against a repository at a base commit, and a conversation trajectory T between the developer and the assistant (user turns, agent tool calls, and messages), the goal is to produce a specification S that is both strong—a satisfactory implementation can be derived from S alone—and abstract—capturing behavioral intent without prescribing implementation. These desiderata are in tension: implementation detail increases strength but reduces abstractness, while aggressive abstraction risks omitting requirements. A good specification is thus abstract where it can be and concrete only where it must be, gated by what an agent can discover from the environment. We do not require the developer to reify their requirements explicitly; instead, we treat requirements as implicit—whatever is observable from the session (the developer’s prompts, corrections, and accepted behaviors) is a sufficient expression of the requirements. We operationalize strength through the regeneration test (Section 3.4): if a blind AI agent, starting from the same base commit, can produce a code change C ′ from S alone such that a three-tier verifier deems C ′ equivalent to C modulo the conversation T , then S is considered strong. The verifier grounds its judgment

4

Given the following conversation and diff, create a specification that another coding agent can use to reimplement the change. Part 1: Specification

Write three short prose sections (no code, identifiers, paths, or line numbers unless essential and undiscoverable): • Intent and Rationale: what the code changes achieve. • Essential Design Decisions: key behaviors/criteria that must be preserved (separate essential from incidental). • Undiscoverable Facts: external names, thresholds, contracts, and domain gotchas an implementer cannot infer from the codebase. Includes file paths or symbol names explicitly requested in the conversation—preserve verbatim. Part 2: Requirements

List the behavioral requirements as concise declarative statements. Focus on outcomes, not implementation. Do NOT include instructions about tests. Figure 5 Extraction prompt for spec distillation (shortened for presentation).

in the task requirements expressed in T , accepting any implementation that conforms to the stated intent regardless of structural differences from C. The environmental grounding hypothesis. The abstractness desideratum rests on a hypothesis: a coding agent can reconstruct substantial contextual information—build configurations, naming conventions, module structure, API contracts—by navigating the repository, rather than requiring the specification to spell it out. If this hypothesis holds, a spec needs to be concrete only for undiscoverable facts: decisions, thresholds, and domain constraints that cannot be inferred from the codebase. Everything else can be stated abstractly, because the agent’s environmental grounding fills the gap.

3.2

Spec Distillation

The distillation stage transforms the raw inputs—the code change C and the conversation trajectory T —into an abstract natural-language specification S. We prompt the LLM with C and T , along with an extraction prompt that instructs it to produce a structured specification in three prose sections—Intent and Rationale, Essential Design Decisions, and Undiscoverable Facts—together with a behavioral checklist of requirements phrased as declarative statements (Figure 5). The extraction prompt enforces abstractness by default: it instructs the LLM to use “no code, identifiers, paths, or line numbers unless essential and undiscoverable,” making concreteness the exception rather than the rule. The three sections operate at different abstraction levels: Intent and Rationale is maximally abstract (pure what and why); Essential Design Decisions sits at mid-level (which approach, but not how to code it); Undiscoverable Facts is necessarily concrete—names, thresholds, and contracts that the agent cannot infer from the environment. Section 2 shows a concrete example of a spec produced by this prompt. This design reflects a key trade-off. A highly structured template (e.g., with separate sections for functional requirements, data model, and error handling) would impose organization on every change, but risks overspecifying simple patches and under-representing concerns that do not fit the template. By contrast, a free-form but intent-focused prompt lets the LLM adapt the level of detail to the complexity of the change.

3.3

Three-Tier Verification

A key design question in AfterVibe is how to determine whether the regenerated code C ′ is functionally equivalent to the original artifact C. We employ a three-tier verification pipeline that combines complementary signals at increasing levels of semantic depth. Each tier is implemented as an autonomous subagent with repository access, placing the verifier collectively in the agent-as-a-judge paradigm (Zhuge et al., 2025)—an extension of the successful LLM-as-a-judge approach (Zheng et al., 2023; Gu et al., 2025). To offset known judgment biases, no single tier is decisive: we combine execution-grounded and reasoning-based signals. Flexible test execution. The first tier runs tests derived from the conversation trajectory—commands the developer executed during the vibe-coding session—against the regenerated code C ′ . Because C ′ may expose slightly different interfaces than the original C, AfterVibe employs a flexible test runner that adapts test 5

harnesses to minor interface changes (e.g., renamed entry points or reordered parameters) rather than failing on superficial mismatches. This flexibility avoids overly prescriptive testing while still verifying that the regenerated code satisfies the behavioral expectations embedded in the session. Verification conditions. The second tier extracts verification conditions (VCs)—testable behavioral properties— from the conversation trajectory T , the code change C, and the human-authored summary M (the diff title, description, and test plan the developer submits for code review). VCs express what the code should do (e.g., “the date-range picker filters all three charts”) without prescribing how. Crucially, VCs are not derived from the spec S, which would make the validation circular. This independence ensures that VCs serve as an unbiased oracle for assessing whether both C and C ′ satisfy the developer’s requirements. This independence also lets the VCs act as a fixed reference point: as we will see later, we iteratively refine the spec S to make it stronger, but we hold the verification conditions constant throughout, so that every candidate spec is judged against the same oracle. Ground-truth alignment. Verification conditions check properties individually; ground-truth alignment checks whether the regeneration makes sense as a whole. Recent work on agentic code reasoning demonstrates that LLM agents can perform meaningful semantic code analysis without executing code (Ugare and Chandra, 2026). The ground-truth alignment checker is an LLM agent that receives the conversation trajectory T , the original code change C, the regenerated code C ′ , and full access to the repository at the base commit. It determines whether C ′ conforms to the intent expressed in T and the behavioral expectations established by C. Equivalence is judged modulo the conversation: because vibe-coded changes are often broad and under-determined, there is no single correct implementation. Any regeneration that conforms to the intent and constraints expressed in the conversation is considered valid, even if it differs substantially from the original in structure, naming, or implementation strategy. Combining tiers. The three complementary tiers each contribute a weighted score to a combined regeneration score (regen_score, 0–6), defined as regen_score = 3 flex + 2 vc + align, where flex ∈ [0, 1] is the fraction of flexible tests that pass, vc ∈ [0, 1] is the fraction of verification conditions satisfied, and align ∈ {0, 1} is the binary ground-truth alignment verdict. The weights encode a deployment-informed priority: executiongrounded tests rank highest (3) as the strongest signal that the regeneration is not broken, verification conditions moderate (2) as independent checks needing no execution infrastructure, and ground-truth alignment lowest (1) to avoid over-rewarding literal reproduction of the reference patch. The weighting is a configurable design choice, and our findings are robust to it: under equal weights, swapped flex/VC weights, and a ground-truthheavy weighting, the AfterVibe-vs-human comparison keeps the same sign and the per-task ranking is preserved (Section 4.8).

3.4

The Regeneration Test

The regeneration test is the core validation mechanism of AfterVibe. A fresh LLM instance—with no access to the original code C or conversation T —receives only the spec S and is asked to implement the artifact from scratch. The intuition is that if the spec is sufficiently strong, a competent implementer (human or AI) should be able to produce a functionally equivalent artifact. Formally, we define the regeneration test as: ( PASS if V (C ′ , C, T ) > τ RegenTest(S, C, T ) = FAIL otherwise

(1)

where V is the three-tier verifier (Section 3.3), C ′ is the code produced by the blind regeneration agent, T is the conversation trajectory providing task context, and τ is a passing threshold. The verifier applies test execution, verification-condition checking, and ground-truth alignment, grounding its judgment in the task requirements expressed in T .

6

3.5

Iterative Spec Refinement

When a task’s regenerated code scores below a threshold (regeneration score < τ , default τ = 6.0), AfterVibe enters a per-task spec strengthening loop that refines the individual specification rather than the global extraction prompt. This feedback-driven refinement follows the iterative generate–critique–improve paradigm shown to be effective for LLM-based program repair, fuzzing, and general-purpose text improvement (Madaan et al., 2023; Xia and Zhang, 2024; Fuz). The strengthening operates at the granularity of individual verification conditions: for each VC that the regenerated code fails, a refinement LLM receives the original spec S, the ground-truth diff C, the regenerated diff C ′ , the failed verification condition, and the grader’s rejection reasoning. It then analyzes why the regeneration diverged from the original intent, identifies what was ambiguous or underspecified in S, and produces a complete rewritten spec S ′ . The refined spec is re-evaluated through the full pipeline: a fresh agent regenerates code from S ′ , and the three-tier verifier grades the result. Best-of-K selection. After K strengthening rounds, AfterVibe keeps the best spec per task —the one that achieved the highest regeneration score across the baseline and all rounds. Only tasks scoring below τ = 6.0 enter the loop; once a task reaches that threshold it exits early. Because the selection takes the per-task maximum, the aggregate score is monotonically non-decreasing by construction: individual rounds may score below the baseline (each is a single noisy rollout), but the best-of-K can only improve or stay the same. Note that strengthening quality is ultimately bounded by the information in the conversation trajectory: a vague or underspecified session yields a weak spec regardless of refinement effort.

4

Evaluation

We evaluate AfterVibe along six research questions: • RQ1 – Regeneration Fidelity: Can a spec distilled from a vibe-coding session let a blind agent regenerate functionally equivalent code? • RQ2 – Spec Strengthening: Can per-task verifier feedback strengthen individual specifications and increase solve rate? • RQ3 – Abstraction vs. Strength: How does specification abstraction relate to regeneration fidelity, and what role does code-token leakage play? • RQ4 – Regeneration Diversity: How similar are passing regenerations from the same spec, relative to natural upper and lower bounds? • RQ5 – Grader Validity: Do the extracted verification conditions and test commands reliably separate correct code from wrong or degraded code? • RQ6 – Comparison with Human-Authored Descriptions: Does AfterVibe produce more effective specs than the commit descriptions developers already write?

4.1

Dataset

4.1.1

Company Internal Dataset (TechInternal)

Our primary evaluation uses real-world coding sessions from an internal AI coding assistant that follows a monorepo-based, incremental software development workflow. We refer to this dataset as TechInternal. Source and curation. We sample multi-turn coding-assistant sessions from a 7-day window. Each session consists of a developer interacting with an AI coding assistant to implement a code change in a large monorepo. Sessions are selected by a curation funnel that filters for: (i) completed sessions with a landed diff, (ii) non-trivial code changes (excluding pure config or generated-file edits), and (iii) sessions with sufficient conversation context for spec extraction. This funnel yields 122 candidate sessions. Ground-truth validation. We validate each candidate through a ground-truth verification run: the verification pipeline is executed against the original landed code—not a regeneration. Two graders run on the original code: the flexible test runner and the verification conditions checker. Ground-truth alignment is skipped because there is no regeneration to compare against. Of the 122 candidates, 81 complete with both graders 7

producing a verdict (the remaining 41 are excluded due to infrastructure failures: evaluation-sandbox crashes, grader-process timeouts, or tool-server startup errors); the excluded tasks have comparable verification-clue counts (median 11 vs. 11), test-manifest counts (median 2 vs. 2), and similar or slightly higher session durations (median 16 min vs. 14 min), consistent with infrastructure retries and timeouts rather than a task-complexity bias. Of the 81 fully graded candidates, 72 pass both graders (88.9% pass rate), forming the final evaluation set. Failure analysis. The 9 ground-truth failures—sessions where the landed, CI-passing code fails at least one grader—stem from three causes. Four are test-command environment mismatches: the LLM-extracted test commands assume developer-machine dependencies (JavaScript runtimes, native shared libraries, device interfaces, or build-graph targets) absent in the evaluation sandbox. Three are test-extraction failures: the LLM extracted zero test commands or a nonexistent test target from the conversation transcript. Two are grading-rule edge cases: the reference patch deletes the only test file, so the grader marks it skipped and conservatively scores the empty result as a failure. None of these 9 represent code regressions—all 122 diffs passed CI and landed successfully. The failures reflect limitations of mining test oracles from conversation context; environment-aware test-command extraction could recover several of these tasks. Characteristics. The 72 validated tasks span typical monorepo development activities: bug fixes, feature additions, refactors, and infrastructure changes. The average original diff is 41,638 characters. Each task has on average 10.5 verification conditions extracted from the conversation trajectory and 1.5 test commands derived from the session. Both verification conditions and test commands are extracted by dedicated LLM-based pipelines.

4.2

Experimental Setup

All LLM components—spec distillation, verification condition and test command extraction, strengthening feedback, and the regeneration agent—use a single frontier large language model. The regeneration agent runs in an agentic harness with code-editing tools, shell access, and automated graders that evaluate the result after each attempt. The distillation prompt follows the template described in Section 3.2. The regeneration agent receives only the vibe spec and a generic instruction to implement the described artifact. Verification artifacts—verification conditions and test commands—are extracted independently from the conversation trajectory using dedicated LLM-based extraction pipelines. Each task is evaluated by the three active graders of the multi-tier verification pipeline (Section 3.3). We report the regeneration score (0–6 scale) as the primary metric. For grader validity (Section 4.7), we also run spec-free negative controls to verify that the extracted verification artifacts have genuine discriminative power—that is, they pass on correct code but fail on wrong or degraded code.

4.3

RQ1: Regeneration Fidelity

For each task, we distill a post-hoc specification from the original conversation and code change C. A fresh agent then receives only this specification and attempts to regenerate the target code change from the same base commit. We compare the regenerated code C ′ against C using the three-tier verification pipeline. The mean regeneration score is 5.06/6.0 (Table 1). Scores are aggregated over the 68 of 72 tasks that produced a complete grader verdict; the remaining four never reached grading and are excluded from the scored aggregates. Inspecting their trajectories shows these were all harness failures rather than model or task failures: one event-serialization crash, one wall-clock timeout, and two startup aborts, and three of the four produced no patch at all. The verification conditions grader achieves the highest individual pass rate (86.8%), followed by flex test execution (72.1%) and ground-truth alignment (66.2%). When requiring all three graders to pass simultaneously (strict conjunction), 54.4% of tasks succeed.

4.4

RQ2: Spec Strengthening

RQ2 asks whether per-task feedback from the three-tier verifier can strengthen individual specifications that failed regeneration. Starting from 72 baseline specs, the strengthening loop (Section 3.5) targets tasks with

8

Table 1 Specification strategy comparison on the TechInternal dataset. Regeneration score is on a 0–6 scale; per-grader

rates are percentages. Human-authored summary = diff title + description + test plan used verbatim as the spec. Strategy

Regen

VC %

Flex %

GT %

Human-authored summary AfterVibe AfterVibe + strengthening

4.23 5.06

64.0 86.8 –

60.0 72.1 –

50.0 66.2 –

5.74

Table 2 Spec strengthening round progression (Section 4.4, 72 tasks, 3 rounds). Per-round metrics are over the failing cohort evaluated that round; the best-of row aggregates over all 68 considered tasks.

Round

Graded

Mean Regen

Flex %

VC %

GT %

Baseline Round 1 Round 2 Round 3

68 31 19 11

5.06 4.68 4.71 4.38

72.1 60.0 55.6 45.5

86.8 86.7 88.9 81.8

66.2 54.8 52.6 45.5

Best-of-K

68

5.74

–

–

–

regeneration score < 6.0: 4 tasks are skipped due to null baselines, leaving 68 considered tasks of which 31 enter strengthening (the remaining 37 already score = 6.0). Each task undergoes up to 3 rounds of refinement, with per-task early exit once regeneration score reaches 6.0. Table 2 shows the round-by-round progression. Per-round regeneration scores are computed over only the failing tasks evaluated that round (not all 68 tasks), so they are naturally lower than the all-task baseline—the two are not directly comparable. The best-of-K row reports the aggregate after keeping the highest-scoring spec per task across baseline and all rounds: the mean regeneration score rises from 5.06 to 5.74 (+0.68 delta) over the 68 considered tasks. Of the 31 tasks that entered strengthening, 26 achieved a positive delta—an 84% success rate. Figure 6 tracks the cumulative best-of-K regeneration score over the failing cohort (N = 31, the same tasks at every round): it climbs steadily from a baseline of 3.93 to 4.99 after round 1, 5.34 after round 2, and 5.51 after round 3, showing that iterative strengthening progressively recovers the failing cohort. At the per-task level, 26 of 31 tasks improve at least once across the three rounds, with many jumping to ≥ 5.5. The graded-task count shrinks from 31 in round 1 to 19 in round 2 and 11 in round 3 as tasks that reach τ early-exit the pool. VC pass rates remain high across rounds (82–89%), while flex-test and GT rates decline in later rounds (flex 60.0% to 45.5%, GT 54.8% to 45.5%), reflecting the increasing difficulty of the residual failing cohort. Strengthening specs in this manner is an instance of loop engineering, where a human gives an optimization target to an agent and let’s it iterate towards a goal.

4.5

RQ3: Abstraction vs. Strength

RQ3 investigates the tension between abstraction and strength: does a more abstract spec—one that captures intent without implementation detail—sacrifice regeneration fidelity? For each task, we compute the compression ratio CompressionRatio(S, C) = |C|chars /|S|chars , where |C|chars is the character length of the ground-truth unified diff and |S|chars is the character length of the generated spec. Higher ratios indicate stronger compression. Three extraction strategies. We compare three spec-extraction configurations spanning the abstraction–detail trade-off: (a) Standard, the default AfterVibe extraction with no length constraint (the Section 4.3 baseline); (b) Constrained (1000c), targeting ∼1,000 characters for maximally abstract, intent-focused specs; and (c) 9

mean regen score (0-6, higher better)

N = 31 failing tasks (same set each round) 5.4 best-of-K kept (cumulative) 5.2 4.99 5.0 4.8 4.6 4.4 4.2 4.0 3.93 baseline

5.51

5.34

r1 r2 strengthening round (0 = baseline)

r3

Figure 6 Cumulative best-of-K regeneration score across 3 strengthening rounds, over the failing cohort (same tasks at

every point).

Table 3 Spec abstraction vs. regeneration quality across three extraction strategies. Higher compression ratio = more

abstract spec; regeneration score on 0–6 scale. Leakage = fraction of the diff’s distinctive code tokens that appear verbatim in the spec. Strategy

Constrained (1000c) Standard Diff-preserving

Spec Avg

Ratio

Regen

Leak %

2,117 6,960 11,836

16.16× 5.69× 2.79×

4.81 5.06

23.7 38.6 62.6

5.55

Diff-preserving, prompted to retain concrete implementation detail (file paths, identifiers, code snippets), yielding specs that approach the original diff size. Table 3 reports the results. At first glance, more concrete specs achieve higher regeneration scores: the diff-preserving variant (2.79× compression) scores 5.55/6.0, outperforming the standard extraction (5.06, 5.69×) and the constrained variant (4.81, 16.16×). Taken at face value, this would suggest that abstractness always hurts—but the leakage column tells a different story. Leakage confound. The diff-preserving spec copies 62.6% of the diff’s distinctive code tokens verbatim (identifiers, literals), compared to 38.6% for standard and 23.7% for constrained. A per-tier breakdown shows that the regeneration score advantage is disproportionately driven by the ground-truth alignment grader (89% vs. 63–66%), which rewards matching the reference patch—exactly what high-leakage enables. The behavioral graders also improve (VC: 91% vs. 81–87%; flex: 87% vs. 66–72%), but the gap is smaller. This suggests that much of the diff-preserving advantage reflects literal code copying rather than better intent communication. The standard extraction offers the best balance of abstractness and strength: meaningful compression (5.69×) with moderate leakage (38.6%) and strong behavioral verification (VC 87%, flex 72%). Abstractness confirmed by diversity. RQ4 provides complementary evidence: passing regenerations from the standard spec are structurally diverse (chrF 0.89, not 1.0), confirming that the spec constrains what without dictating how —the hallmark of a well-abstracted specification. The constrained strategy maintains tight spec lengths (∼2,100 chars) regardless of diff size, while the diff-preserving strategy scales with diff length (Figure 7).

10

60000

AfterVibe constrained AfterVibe (c1000) diff preserving spec = original

spec length (chars)

50000 40000 30000 20000 10000 0

0

10000 20000 30000 40000 50000 60000 original diff length (chars)

Figure 7 Per-task spec length vs. original diff length for the three strategies (axes capped at 60K chars); the dashed

line marks spec = original.

4.6

RQ4: Regeneration Diversity

RQ4 measures how much independent regenerations vary when conditioned on the same specification. For each of the 72 tasks, we run the regeneration agent 3 times from the same base commit and specification, yielding 200 task-pairs for pairwise comparison (of the 216 possible pairs, 16 are skipped because one rollout produced no patch). Similarity metrics. We compare each pair of regenerated patches at the file level using two complementary measures: chrF (character n-gram F-score, normalized to [0, 1] via sacrebleu) captures character-level overlap and is robust to minor formatting differences; difflib ratio (Python SequenceMatcher) captures sequence-level structural similarity. For each task-pair, we take the union of files touched by either patch; files present on only one side score 0.0, and files present on both sides are scored independently. The task-level similarity is the mean of per-file scores. Outcome segmentation. To relate code diversity to verification outcome, we segment task-pairs by whether both regenerations pass (regeneration score ≥ 5.5), both fail, or one passes and the other fails (“mixed”). This threshold matches the pass-to-pass anchor below, so the both-pass segment and that anchor cover the same 83 rollout pairs. Across the 200 task-pairs, both-pass pairs show the highest code agreement (chrF 0.888, difflib 0.819), confirming that passing specifications reliably guide agents toward similar solutions. Both-fail pairs remain nearly as similar (0.856/0.749)—under-specified specs drive independent agents toward the same incorrect solution, a signal of systematic rather than random spec gaps—while mixed-outcome pairs are least similar (0.835/0.740), consistent with genuine divergence driving the split outcome (overall 0.858/0.771).

11

Table 4 Negative control results (Section 4.7), conditioned on the TechInternal tasks whose correct code passes both VC and flex (ground truth = 100% by construction). Lower pass rates on worse code indicate stronger discriminative power.

Code quality

Correct (ground truth) Partial (50% hunks removed) Pre-change (before change) Wrong (permutation)

Jobs

VC %

Flex %

72 66 69 70

100.0% 47.0% 0.0% 1.4%

100.0% 42.4% 58.0% 51.4%

Cross-rollout stability. Across the 3 rollouts, the per-task regeneration score is stable (rollout means of 5.06, 4.87, and 4.99; mean per-task standard deviation 0.49), and within-task code agreement is high (both-pass chrF 0.89). Independent regenerations from the same spec thus converge on functionally equivalent solutions while still varying in structure. Reference anchors (patch-level). To calibrate the similarity values, we compare rollout-pair similarity against two reference points using added-lines-only patches: (i) upper bound —each patch vs. itself with one added line removed (mean chrF 0.982); (ii) lower bound —cross-task pairs of unrelated patches (mean chrF 0.180). Pass-to-pass rollout pairs (both regeneration score ≥ 5.5) achieve chrF 0.899, sitting much closer to the upper bound than the lower bound. This confirms that the specification constrains the solution space far beyond what would be expected by chance, while still permitting minor structural variation.

4.7

RQ5: Grader Validity

RQ5 asks whether the extracted verification conditions and flex tests genuinely discriminate correct code from incorrect code—that is, whether they are valid oracles rather than superficial checks that pass on any input. We answer with three spec-free negative controls: the same verification conditions and test commands used in ground-truth validation (Section 4.1.1) are run against degraded, pre-change, or wrong code instead of the original landed code. No specification or regeneration agent is involved; only the code varies, so any difference in grader pass rate directly measures discriminative power. Pre-change control (before the change). Each task keeps its own oracle (verification conditions and test commands) but is graded against the repository state before the task’s code was landed (the parent commit). If task A’s VCs still pass on the pre-change checkout, the VCs are not checking the task’s intended behavior. Degradation control (partial code). An LLM removes approximately 50% of each task’s diff hunks (whole hunks, syntax-preserving), then the task’s own VCs and tests run against the degraded code. If VCs do not notice the missing functionality, they lack coverage. Permutation control (wrong code). Each task A keeps its own oracle but is graded against a different task B’s landed code, assigned by a seeded derangement (Sattolo’s algorithm—a single-cycle permutation with no fixed points, so every task receives unrelated code). If task A’s VCs still pass on task B’s code, the VCs are not checking task-specific intent. Table 4 reports the conditioned view: restricting to 72 tasks where correct code passes both graders (ground truth = 100% by construction), we measure how often each grader also passes degraded, pre-change, or wrong code. The verification-clues grader exhibits sharp monotonic discrimination: 100% on correct code → 47% on partial → near-zero on pre-change (0%) and wrong code (1.4%). Not a single task’s verification conditions pass on the repository state before the change was landed, and only 1 of 70 passes on an unrelated task’s code, confirming that VCs check task-specific behavioral intent rather than surface properties. The flex-test grader drops to 42% on partial code but remains elevated on pre-change (58%) and wrong code (51%)—because many test commands pre-exist the change and can pass on unrelated code that happens to compile (e.g., “build the target”). Figure 8 visualizes the conditioned pass rates: VC’s sharp staircase (100% → 47% → 0–1%) confirms strong task-specific discrimination. These results validate the ground-truth filtering of 12

Correct code (ground truth) Partial code (degradation 50%)

VC pass rate

100.0 47.0 0.0 1.4

Flex test pass rate

100.0 42.4 58.0 51.4

Pre-change code (before change) Wrong code (permutation)

0 20 40 60 80 100 pass rate on GT-passing tasks (%, verdict-only) Figure 8 Per-grader pass rates by code condition, conditioned on the 72 tasks whose correct code passes both VC and

flex.

Section 4.1.1: tasks whose VCs pass on correct code are genuine positive signals, not false positives from overly permissive oracles.

4.8

RQ6: Comparison with the Human-Authored Summary

RQ6 asks whether the structured extraction of AfterVibe produces specifications that are more effective for regeneration than the descriptions developers already author as part of their normal workflow. We compare against a human-authored baseline: the human-authored summary that the developer submits for code review—consisting of the diff title, description, and test plan—used verbatim as the specification. The regeneration agent, three-tier grading pipeline, and evaluation infrastructure remain identical across both conditions, isolating the effect of the specification source. Table 1 includes the comparison. AfterVibe achieves a mean regeneration score of 5.06, compared to 4.23 for the human-authored summary—a difference of 0.82 points on the 0–6 scale, with a consistent gap across all three graders.3 The human-authored summary is shorter on average (2,129 vs. 6,960 characters), yet captures less of the intent required for successful regeneration. This result is consistent with the intended audience of each artifact. The human-authored summary is written for human reviewers who have access to the accompanying code; it describes what changed at a high level but typically omits the behavioral constraints, design decisions, and undiscoverable facts that a blind regeneration agent requires. AfterVibe’s structured extraction recovers precisely these elements from the conversation trajectory, producing specifications that are more verbose but substantially more effective as self-contained implementation guides.

4.9

Implication of Results

Our results offer empirical support for the environmental grounding hypothesis (Section 3.1). The high pass rate after refinement suggests that agents already extract substantial context from the repository environment— build configurations, existing module structure, naming conventions—without this information appearing in 3 Robust to weighting: under equal (2, 2, 2), swapped (2, 3, 1), and GT-heavy (1, 2, 3) weights, the AfterVibe-vs-human gap stays 0.82–0.89 points and the per-task ranking is unchanged (Spearman ≥ 0.97).

13

the spec. This has a provocative implication: much of what we traditionally consider “specification” is actually shared knowledge that a grounded agent can infer from the codebase. The useful part of a specification—the part that needs to be explicitly written—consists primarily of project-specific decisions that cannot be derived from the environment. This perspective clarifies the abstractness goal of Section 3.1: a spec should be concrete only for facts the agent cannot discover from the environment, and abstract for everything else. As mentioned earlier, our vision is that such specifications can supplant code as the artifact of human review and even the source of record; exploring these possibilities in industrial practice is future work.

5

Threats to Validity

Internal validity. Our oracle is LLM-generated, so the test suite could encode hallucinated or trivial behavior. We address this by validating every generated test against the original landed code, ensuring the suite encodes actual—not hallucinated—behavior; the negative-control analysis of Section 4.7 further shows that the verification conditions sharply separate correct code from degraded, pre-change, and unrelated code. A second threat is reconstruction variance: because agents are non-deterministic, regenerating from the same specification can yield different regen_scores across runs. We quantify this through the cross-rollout diversity analysis of Section 4.6, which shows that independent regenerations remain functionally stable (per-task regen_score standard deviation of 0.49) while varying in surface structure. Finally, there is a risk of information leakage between spec extraction and regeneration: if a single agent extracted the specification and then regenerated the code immediately afterward, it could still hold the original code in its context and reproduce it from memory rather than from the specification, inflating scores. We address this by separating the two stages into distinct sessions with no shared context, so the regenerating agent sees only the specification and cannot fall back on the original code. External validity. Our dataset consists of 72 tasks drawn from coding-assistant sessions, which may not be

representative of all vibe-coded software or generalize to other languages, domains, or developer populations; we mitigate this by sampling tasks from real coding-assistant sessions rather than synthetic benchmarks, grounding the evaluation in genuine developer activity. In addition, all experiments use a single frontier LLM, and because specification quality depends on model capability, our results may not generalize to other or weaker LLMs.

6

Related Work

AfterVibe draws on several lines of research concerned with specification extraction and its uses.

6.1

Spec-Driven Development

Recent industry tools such as GitHub SpecKit (GitHub, 2025) and Amazon Kiro (Amazon Web Services, 2025) have recently adopted spec-first workflows, requiring developers to author specifications upfront and maintain them alongside code. All of these approaches—from Design by Contract to modern spec-first IDEs—assume that specifications are written before or during coding. AfterVibe delivers similar benefits post-hoc, recovering specifications from sessions where none were written, making it compatible with vibe coding by construction. Kiro in particular uses the EARS notation (Mavin et al., 2009) (Easy Approach to Requirements Syntax) for its requirements.md, a small set of semi-formal templates that constrain otherwise unstructured natural-language requirements. AfterVibe’s verification conditions are themselves naturallanguage rubrics, and recent LLM-based methods have shown that such requirements can be autoformalized into EARS or related semi-formal templates (Imran et al., 2025; Roßkothen et al., 2026; Giannakopoulou et al., 2021). AfterVibe could therefore act as an entry point from vibe coding into spec-driven development. Recasting code changes into natural language is also the goal of code summarization and commit-message generation (Liu et al., 2018, 2022; Feng et al., 2020); our specifications differ in that they must be precise enough to regenerate the change, not merely describe it. Traditional approaches, too, require writing specifications before or during implementation. Meyer’s Design by Contract (Meyer, 1992) mandates pre- and postconditions written before code, with runtime checking 14

enforcing compliance. Test-driven development encodes intent as executable specifications that precede the code under test. More recently, TiCoder (Fakhoury et al., 2024) formalizes user intent interactively during LLM-based code generation through iterative test refinement.

6.2

LLM-Based Specification Extraction

Close technical relatives of AfterVibe are systems that extract specifications from code. SpecGen (Ma et al., 2025) generates formal JML specifications from Java methods using LLMs combined with mutation testing and static analysis to filter incorrect candidates. AutoSpec (Wen et al., 2024) produces Dafny specifications through LLM-driven counterexample-guided refinement. Endres et al. (Endres et al., 2024) generate postconditions from natural-language docstrings, validated against existing test suites. SpecRover (Ruan et al., 2025) iteratively extracts code intent from buggy code and issue descriptions to guide automated patch generation. All of these systems derive specifications from code or domain knowledge alone. AfterVibe differs in two ways: it extracts from the agent trajectory—conversation and diff together—using the conversation as a richer signal of developer intent; and it produces natural-language specs validated through regeneration rather than formal annotations tied to a specific verification framework.

6.3

Specification Verification and Quality

A fundamental challenge in specifications is knowing whether the spec is correct. VeriAct (Misu et al., 2026) shows that verifier-accepted Dafny specs are often semantically wrong, and Le Cong et al. (Le-Cong et al., 2025) question whether LLM-generated specs capture true semantics or merely surface patterns. Lahiri frames intent formalization as a grand challenge (Lahiri, 2026) and proposes grounding spec correctness in concrete input-output examples (Lahiri, 2024). On the formal side, AutoVerus (Yang et al., 2025) generates machinechecked proofs of Rust code from specifications, and Verus-SpecGym (Agarwal et al., 2026) benchmarks natural-language-to-formal autoformalization—notably finding that execution-based checking catches spec errors that LLM-as-judge evaluation misses. These approaches rely on formal verification, symbolic checking, or executable formal specifications. AfterVibe’s answer is pragmatic: a spec is correct if it can regenerate functionally equivalent code, validated by a multi-tier pipeline—no theorem proving required. It works in the opposite direction, recovering naturallanguage specs post-hoc rather than formalizing intent up front, and thus operationalizes Lahiri’s vision without formal specification languages. The Kiro team (Kiro Team, 2026) similarly use LLM reasoning to elicit tests from informal requirements, echoing our extraction of verification conditions from conversations.

6.4

Agent Trajectories as Artifacts

An emerging body of work uses or produces trajectory data from coding agents. Zhu et al. (Zhu et al., 2026) generate specifications from failing tests and natural-language descriptions, then use them to guide program repair. RECODE-H (Miao et al., 2025) benchmarks iterative code generation with multi-level human feedback, treating the full interaction as a trajectory. TrajAudit (Wang et al., 2026) also operates on agent trajectories, but for failure diagnosis—localizing where and why an agent went wrong rather than capturing what it achieved. These works use trajectories to generate code, benchmark interactions, or diagnose failures. AfterVibe instead treats trajectories as a specification source, extracting self-validating verification conditions and regeneration specifications from the conversation record. AfterVibe is, to our knowledge, the first system to use agent coding trajectories—conversation and diff together—for post-hoc intent capture.

7

Conclusion

We have presented AfterVibe, a framework for distilling verifiable specifications from vibe-coded artifacts. By extracting structured specs and validating them through a regeneration test backed by a three-tier verification pipeline—flexible test execution, independent verification conditions, and ground-truth alignment— AfterVibe bridges the gap between the ease of vibe coding and the rigor of traditional software engineering.

15

Our evaluation measures whether extracted specs can regenerate ground-truth diffs, how the level of abstraction relates to regeneration fidelity, how much independent regenerations vary, and whether feedback can strengthen individual specs. We believe that specifications—not code—should become the primary artifact of human authorship in the age of AI-assisted development, and AfterVibe is a first step toward realizing this vision.

Data Availability We provide the full pipeline prompts as supplementary material for reproducibility—and, to our knowledge, no human vibe-coding trajectory dataset with execution environments is yet openly available.

Acknowledgments Use of generative AI. We disclose that generative AI was used throughout this work—drafting text, writing analysis scripts, processing data, and generating tables—with all output reviewed and verified by the authors, who take full responsibility for the final manuscript.

References Fuzz4All: Universal Fuzzing with Large Language Models | Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. https://dl.acm.org/doi/10.1145/3597503.3639121. Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, Seungone Kim, Jannis Limperg, Cedric Flamant, Kanna Shimizu, Bryan Parno, and Sean Welleck. Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization. https://arxiv.org/abs/2605.26457v1, May 2026. Amazon Web Services. Kiro: Move beyond AI coding to agentic engineering, 2025. Alberto Bacchelli and Christian Bird. Expectations, outcomes, and challenges of modern code review. In 2013 35th International Conference on Software Engineering (ICSE), pages 712–721, May 2013. doi: 10.1109/ICSE.2013. 6606617. Liming Chen and Algirdas Avizienis. N-version programming: A fault-tolerance approach to reliability of software operation. In Digest of Papers, FTCS-8: Eighth Annual International Conference on Fault-Tolerant Computing, pages 3–9, Toulouse, France, 1978. DORA. State of AI-assisted software: DORA report. https://dora.dev/research/2025/dora-report/, 2025. URL https://dora.dev/research/2025/dora-report/. Online; DORA (DevOps Research and Assessment), Google Cloud. Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K. Lahiri. Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? Proceedings of the ACM on Software Engineering, 1(FSE):84:1889–84:1912, July 2024. doi: 10.1145/3660791. Sarah Fakhoury, Aaditya Naik, Georgios Sakkas, Saikat Chakraborty, and Shuvendu K. Lahiri. LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation. IEEE Transactions on Software Engineering, 50(9):2254–2268, September 2024. ISSN 1939-3520. doi: 10.1109/TSE.2024.3428972. Zhangyin Feng, Daya Guo, Duyu Tang, Nan Duan, Xiaocheng Feng, Ming Gong, Linjun Shou, Bing Qin, Ting Liu, Daxin Jiang, and Ming Zhou. CodeBERT: A Pre-Trained Model for Programming and Natural Languages. In Trevor Cohn, Yulan He, and Yang Liu, editors, Findings of the Association for Computational Linguistics: EMNLP 2020, pages 1536– 1547, Online, November 2020. Association for Computational Linguistics. doi: 10.18653/v1/2020.findings-emnlp.139. Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, and Johann Schumann. Automated formalization of structured natural language requirements. Information and Software Technology, 137:106590, September 2021. ISSN 0950-5849. doi: 10.1016/j.infsof.2021.106590. GitHub. Spec kit: Toolkit for spec-driven development, 2025. O.C.Z. Gotel and C.W. Finkelstein. An analysis of the requirements traceability problem. In Proceedings of IEEE International Conference on Requirements Engineering, pages 94–101, April 1994. doi: 10.1109/ICRE.1994.292398.

16

Jiawei Gu, Xuhui Jiang, Zhichao Shi, Hexiang Tan, Xuehao Zhai, Chengjin Xu, Wei Li, Yinghan Shen, Shengjie Ma, Honghao Liu, Saizhuo Wang, Kun Zhang, Yuanzhuo Wang, Wen Gao, Lionel Ni, and Jian Guo. A Survey on LLM-as-a-Judge, October 2025. Muhammad Huzaifa Imran, Touseef Tahir, Bilal Hassan, and Hamid Jahankhani. Automated EARS-Based Requirements Generation with Lightweight Large Language Models. In 2025 IEEE International Conference on Technology Management, Operations and Decisions (ICTMOD), pages 1–6, October 2025. doi: 10.1109/ICTMOD66732.2025. 11371998. Kiro Team. Deep dive: Spec analysis and requirements verification in Kiro. Kiro Blog, https://kiro.dev/blog/, 2026. URL https://kiro.dev/blog/. Kiro Blog. John C. Knight and Nancy G. Leveson. An experimental evaluation of the assumption of independence in multiversion programming. IEEE Transactions on Software Engineering, SE-12(1):96–109, January 1986. ISSN 1939-3520. doi: 10.1109/TSE.1986.6312924. Shuvendu K. Lahiri. Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. In Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024, pages 142–147. TU Wien Academic Press, October 2024. ISBN 978-3-85448-065-5. doi: 10.34727/2024/isbn.978-3-85448-065-5_19. Shuvendu K. Lahiri. Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents, March 2026. Thanh Le-Cong, Bach Le, and Toby Murray. Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference, May 2025. Shangqing Liu, Cuiyun Gao, Sen Chen, Lun Yiu Nie, and Yang Liu. ATOM: Commit Message Generation Based on Abstract Syntax Tree and Hybrid Ranking. IEEE Transactions on Software Engineering, 48(5):1800–1817, May 2022. ISSN 1939-3520. doi: 10.1109/TSE.2020.3038681. Zhongxin Liu, Xin Xia, Ahmed E. Hassan, David Lo, Zhenchang Xing, and Xinyu Wang. Neural-machine-translationbased commit message generation: How far are we? In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE ’18, pages 373–384, New York, NY, USA, September 2018. Association for Computing Machinery. ISBN 978-1-4503-5937-5. doi: 10.1145/3238147.3238190. Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE), pages 16–28, April 2025. doi: 10.1109/ICSE55347.2025.00129. Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. SELF-REFINE: Iterative refinement with self-feedback. In Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS ’23, pages 46534–46594, Red Hook, NY, USA, December 2023. Curran Associates Inc. Alistair Mavin, Philip Wilkinson, Adrian Harwood, and Mark Novak. Easy Approach to Requirements Syntax (EARS). In Proceedings of the 2009 17th IEEE International Requirements Engineering Conference, RE, RE ’09, pages 317–322, USA, August 2009. IEEE Computer Society. ISBN 978-0-7695-3761-0. doi: 10.1109/RE.2009.9. B. Meyer. Applying ’design by contract’. Computer, 25(10):40–51, October 1992. ISSN 1558-0814. doi: 10.1109/2.161279. Chunyu Miao, Henry Peng Zou, Yangning Li, Yankai Chen, Yibo Wang, Fangxin Wang, Yifan Li, Wooseong Yang, Bowei He, Xinni Zhang, Dianzhi Yu, Hanchen Yang, Hoang H. Nguyen, Yue Zhou, Jie Yang, Jizhou Guo, Wenzhe Fan, Chin-Yuan Yeh, Panpan Meng, Liancheng Fang, Jinhu Qi, Wei-Chieh Huang, Zhengyao Gu, Yuwei Han, Langzhou He, Yuyao Yang, Yinghui Li, Hai-Tao Zheng, Xue Liu, Irwin King, and Philip S. Yu. RECODE-H: A Benchmark for Research Code Development with Interactive Human Feedback, October 2025. Md Rakib Hossain Misu, Iris Ma, and Cristina V. Lopes. VeriAct: Beyond Verifiability – Agentic Synthesis of Correct and Complete Formal Specifications, March 2026. Julian Roßkothen, Dominik Fuchß, Florian Erdösi, Maria Floruß, Jan Keim, and Tobias Hey. On Converting Natural Language Requirements into Semi-Formal Templates Using LLMs. In 2026 IEEE 34th International Requirements Engineering Conference (RE), 2026. Haifeng Ruan, Yuntong Zhang, and Abhik Roychoudhury. SpecRover: Code Intent Extraction via LLMs. In 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE), pages 963–974, April 2025. doi: 10.1109/ICSE55347.2025.00080.

17

Shubham Ugare and Satish Chandra. Agentic Code Reasoning, March 2026. Minxing Wang, Xiaofei Xie, and Yintong Huo. TrajAudit: Automated Failure Diagnosis for Agentic Coding Systems, May 2026. Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung, and Cong Tian. Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program Verification. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification, pages 302–328, Cham, 2024. Springer Nature Switzerland. ISBN 978-3-031-65630-9. doi: 10.1007/978-3-031-65630-9_16. Chunqiu Steven Xia and Lingming Zhang. Automated Program Repair via Conversation: Fixing 162 out of 337 Bugs for $0.42 Each using ChatGPT. In Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024, pages 819–831, New York, NY, USA, September 2024. Association for Computing Machinery. ISBN 979-8-4007-0612-7. doi: 10.1145/3650212.3680323. Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. AutoVerus: Automated Proof Generation for Rust Code. Proceedings of the ACM on Programming Languages, 9(OOPSLA2):396:3454–396:3482, October 2025. doi: 10.1145/3763174. Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. Judging LLM-as-a-judge with MT-bench and Chatbot Arena. In Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS ’23, pages 46595–46623, Red Hook, NY, USA, December 2023. Curran Associates Inc. Taohong Zhu, Lucas C. Cordeiro, Mustafa A. Mustafa, and Youcheng Sun. Specification Vibing for Automated Program Repair, February 2026. Mingchen Zhuge, Changsheng Zhao, Dylan R. Ashley, Wenyi Wang, Dmitrii Khizbullin, Yunyang Xiong, Zechun Liu, Ernie Chang, Raghuraman Krishnamoorthi, Yuandong Tian, Yangyang Shi, Vikas Chandra, and Jürgen Schmidhuber. Agent-as-a-Judge: Evaluate Agents with Agents. In Proceedings of the 42nd International Conference on Machine Learning, pages 80569–80611. PMLR, October 2025.

18

A

Prompt Artifacts

This appendix reproduces, verbatim, the full prompt suite behind AfterVibe’s post-hoc specification and verification pipeline (section 3), released as supplementary material (section 7). Each box is a single artifact read directly from our released prompt package; template placeholders of the form {...} are left unfilled so the exact prompt as run is visible. The artifacts fall into two groups: the specification and extraction prompts that distill a reusable specification, verification conditions, and a runnable test manifest from a coding session (section A.1), and the multi-tier verification graders that score code regenerated from a specification (section A.2).

A.1

Specification and Extraction Pipeline

These five prompts run over a coding session (its conversation plus the resulting diff) to produce the abstract specification and the evidence used to verify code later regenerated from it. Prompt A.1 – Specification Creation

Distills a structured, abstract specification from a code change and its originating conversation so a blind coding agent can regenerate functionally equivalent code. Given the following conversation and diff , create a specification that another coding ,→ agent can use to reimplement the change . ## Part 1: Specification Write three short prose sections ( no code , identifiers , paths , or line numbers unless ,→ essential and und iscoverable ) : − ∗∗ Intent and Rationale ∗∗: what the code changes in the conversation and diff achieve − ∗∗ Essential Design Decisions ∗∗: the key behaviors / criteria that must be preserved ,→ ( separate essential decisions from incidental impleme ntation choices ) . − ∗∗ U ndiscove rable Facts ∗∗: external names , thresholds , contracts , and domain gotchas ,→ an implementer cannot infer from the codebase . This includes any exact file paths , ,→ filenames , or symbol names the user explicitly requested in the conversation — ,→ preserve those verbatim , since they are a required part of the contract . ## Part 2: Requirements List the behavioral conditions a reviewer would check , each phrased as a declarative ,→ statement . Focus on behavior , not code structure . Avoid over − specificity that would ,→ match only one impleme ntation . Focus on OUTCOMES , not IMPLEMEN TATION . Avoid : − File names , function names , or variable names — UNLESS the user explicitly specified ,→ that exact name or path in the conversation , in which case it is a hard requirement : ,→ keep it verbatim and add a requirement stating that the named artifact exists and ,→ behaves as asked − Impl ementati on details or code snippets − Line numbers or specific code locations − Mentioning changes explicitly The spec should allow someone to verify correctness WITHOUT reading the actual code . ## CRITICAL : Test File Handling Do NOT include instructions to add , modify , or write tests , and do NOT add verification ,→ conditions about test coverage or tests passing . Test changes are already present in ,→ the working directory ; focus only on the non − test production code . Conversation context : ``` { conversation_context } ``` Unified Diff : ``` { unified_diff }

19

```

Prompt A.2 – Per-Task Specification Strengthening

Rewrites a specification whose regenerated code scored below threshold, used in a best-of-K-over-rounds loop that keeps the highest-scoring specification per task. You are refining a specification that failed the regeneration test . A blind coding ,→ agent was given only the specification below and asked to reimplement a code change ,→ from scratch ; the regenerated code did not satisfy one of the behavioral ,→ verification conditions expected of the original change . Your task is to analyze why the regeneration diverged from the original intent , ,→ identify what was ambiguous or underspe cified in the specification , and produce a ,→ complete rewritten specification that closes that gap . Output the full rewritten ,→ specification — not a diff , not a list of edits — so it can be used on its own by a ,→ fresh agent that has never seen the original code or conversation . ## Inputs ORIGINAL SPECIFICATION ( S ) : ``` { original_spec } ``` GROUND − TRUTH CODE CHANGE ( C ) : ``` { g r o u n d _ t r ut h _d i ff } ``` REGENERATED CODE CHANGE (C ') produced from the specification above : ``` { r e g e n e r a t e d_ dif f } ``` FAILED VERIFICATION CONDITION ( a behavioral property the regeneration did not satisfy ) : ``` { failed_verification_condition } ``` GRADER ' S REJECTION REASONING : ``` { grader_rejection_reasoning } ``` ## Analysis instructions 1. Compare the ground − truth change ( C ) with the regenerated change (C ') and pinpoint ,→ where the regeneration diverged from the intended behavior . 2. Identify what in the original specification ( S ) was ambiguous , missing , or ,→ undersp ecified such that a competent implementer produced the divergent behavior — ,→ focus on the failed verification condition and the grader ' s reasoning . 3. Rewrite the specification so that the failed behavior is now unambiguously required , ,→ while keeping the spec abstract : describe outcomes and essential design decisions , ,→ not code structure . Do not over − specify to a single implementation , and do not leak ,→ function names , variable names , paths , or line numbers unless they are ,→ undisco verable external contracts . 4. Preserve everything in the original specification that was already correct ; only ,→ strengthen what led to the failure . ## Output requirements − Output the COMPLETE rewritten specification (S ') , self − contained and ready for a ,→ fresh regeneration agent .

20

− Keep the same overall structure as the original : the three prose sections ( Intent and ,→ Rationale , Essential Design Decisions , Undis coverabl e Facts ) plus the declarative ,→ requirements checklist . − Do NOT include instructions to add , modify , or write tests , and do NOT add ,→ verification conditions about test coverage or tests passing . − The rewritten spec must allow someone to verify correctness WITHOUT reading the ,→ actual code .

Prompt A.3 – Verifiable-Condition Extraction

Pulls structured, provenance-tagged verification conditions out of the session evidence for later checking against regenerated code. Extract structured verification clues from the source coding − agent evidence bundle . A verification clue is a unique , checkable YES / NO question about behavior , scope , user ,→ corrections , or acceptance criteria that generated code C ' should satisfy . Existing ,→ graders still inspect the final code diff , so each clue must remain concise and ,→ independently answerable . Return JSON with ` verification_clue_records `. Each record must include : − ` clue_id `: stable raw id such as " raw_0001 ". − ` clue `: the verification clue string , phrased as a YES / NO question . − ` provenance `: one or more evidence objects . − ` unsupported_by `: include " f i n al _ u n i f i e d _ d i f f " when the final diff does not directly ,→ support the clue . − ` extraction_stage `: use " raw_ex traction ". − ` pre_dedup_clue_ids `: include the record ' s raw id . − ` abstraction_level `: one of " user_goal " , " b e h a v i o r a l _ c o n t r a c t " , " api_surface " , or ,→ " i m p l e m e n t a t i o n _ d e t a i l ". Classify how specific the clue is . Prefer " user_goal " or ,→ " b e h a v i o r a l _ c o n t r a c t ". Only use " i m p l e m e n t a t i o n _ d e t a i l " when the user explicitly ,→ requested that exact detail . Allowed provenance ` source_type ` values : − conversation − metadata − f i n a l _ u ni f i e d _d i f f − test_commands − unknown Rules : − Return only clues grounded in the evidence bundle . − Prefer 5 −15 concise clues when available . − Deduplicate duplicate or near − duplicate clues . − Phrase each clue as a YES / NO question a reviewer can answer from the code diff . − Do not include vague clues such as " Does the code work correctly ?". − Prefer outcome − level product or API contract clues over impl ementatio n mechanics . − Include implementatio n details only when the conversation makes them acceptance ,→ criteria . − Avoid clues about imports , private attributes , helper function names , file layout , or ,→ build graph changes unless the conversation makes that exact detail part of the ,→ requested contract . − Apply the counter factual test : a good clue should be answerable YES for any correct ,→ impleme ntation of the user ' s request , not only the specific implem entation in this ,→ diff . If a clue would be answerable YES only with the exact same variable names , ,→ file layout , or internal API calls , it is too specific — rewrite it as a behavioral ,→ or contract − level question . − Set ` not_supported_by_final_diff ` whenever no ` final_unified_diff ` provenance ,→ directly supports the clue . Better clue style : − Good : " Can personal and project coding − agent memory be routed to the memory service ,→ independently behind separate rollout gates ?"

21

− Good : " Does project memory remain project − scoped when routed through the memory ,→ service , while personal / session memory remains viewer − scoped ?" − Good : " Do memory − service read failures fall back to directory listing before ,→ surfacing a not − found error ?" − Too implementation − specific : " Does A g e n t M e m o r y E x t e n s i o n import M e m o r y C l i e n t F a c t o r y in ,→ a TYPE_CHECKING block ?" − Too implementation − specific : " Is a private ` _memory_storage ` attribute initialized to ,→ None ?" − Too test − specific : " Are two tests named ,→ ` t e s t _ s t o r a g e _ r e n a m e _ p e r s o n a l _ d e l e g a t e s _ t o _ m e m o r y ` added ?" Exclusions — do NOT include clues about : − Intermediate agent actions , tool calls , or debugging steps ( e . g . " the agent searched ,→ for X " , " validation was run ") . − External system state not part of the diff ( e . g . feature − flag or config − service ,→ metadata , spreadsheet contents , dashboard outputs , database state , API responses ) . − Test execution outcomes ( e . g . " all tests should pass " , " code should pass linting " , " N ,→ tests pass ") . Test running is handled by a separate grader . − Test existence or test coverage ( e . g . " a test should be added " , " tests should be ,→ updated ") . Test verification is handled by a separate grader . − Analysis outputs , numeric results , or data artifacts produced during the conversation ,→ that are not part of the code change . Focus exclusively on what the code diff should contain : behavioral changes , structural ,→ modifications , API usage patterns , removed / added logic , and correctness invariants . Conversation context : ``` { conversation_context } ``` Metadata JSON : ``` json { metadata_json } ``` Final unified diff : ``` diff { unified_diff } ```

Prompt A.4 – Test-Manifest Extraction

Distills a runnable test manifest (shell commands) from the session so regenerated code can be checked by execution. Extract a runnable test manifest from source coding − agent validation evidence . Rules : − Return only JSON objects with command and category . − Commands must be self − contained and runnable from the repository root . − If a command must run from a subdirectory , include an explicit relative ` cd path && ,→ ... `. − Prefer observed test tool calls and shell commands over prose summaries . − Convert observed ` run_test ` , ` run_tests ` , and ` run_test_with_coverage ` tool args into ,→ shell commands . − Read the conversation chr onol ogi ca ll y . If older validation commands conflict with later validation commands , keep only the latest final validation commands . − Exclude tests for files , classes , or commands that the later conversation says were deleted , renamed , replaced , removed , obsolete , or no longer referenced . − Prefer commands from final " Verification " , " Validated " , " Done " , or summary sections over commands from early exploration or intermediate stack edits . − Prefer concise smoke coverage over exhaustive historical retries . Keep the strongest 1 −3 final commands unless more are explicitly required . − Do not output raw JSON tool args as commands . − Include build / lint commands when they were used as correctness checks .

22

− Use category " regression " for commands from the original validation flow . − Use category " new " only for additional validation commands clearly requested or ,→ proposed . − Do not invent build targets , file paths , package scripts , or setup commands . − Do not convert table names , product abbreviations , or package labels into repo paths . − Do not include dependency installation , server startup , file inspection , or ,→ data − query commands . − If the conversation says tests passed but does not show the command , return no ,→ command for that claim . Test command conversion examples : − Observed `{{" test_file_pa th ":"/ path / to / repo / frontend / lib / foo / __tests__ / FooTest . js "}} ` −> ` jest frontend / lib / foo / __tests__ / FooTest . js ` − Observed `{{" test_class ":" FooTest "}} ` −> ` test − runner FooTest ` − Observed `{{" test_name ":" FooTest :: testSomething "}} ` −> ` test − runner FooTest :: testSomething ` − Observed `{{" test_file_pa th ":"/ path / to / repo / backend / example / tests / test_foo . py "}} ` −> ` python −m pytest backend / example / tests / test_foo . py ` − Observed `{{" file_path ":"/ path / to / repo / backend / example / tests / test_foo . py "}} ` −> ` python −m pytest backend / example / tests / test_foo . py ` − Observed `{{" test_file_pa th ":"/ path / to / repo / backend / example / FooTest . cpp "}} ` −> no command unless a build target or concrete command is also present . − Observed a build − system test command with an explicit target ( e . g . ` build − tool test ,→ // project / tests : test_manifest_extractor `) −> keep the build − system test command . − Observed a build − system build command with an explicit target ( e . g . ` build − tool build ,→ // project : run_optimizer `) −> keep the build − system build command . − Observed ` cargo test ` without a working directory −> keep it only if the surrounding context makes the repository − root command correct . − Observed ` run_test ` / ` run_tests ` with empty args `{{}} ` −> no command . − Older observed ,→ `{{" test_fil e_path ":"/ path / to / repo / frontend / lib / foo / __tests__ / OldTest . js "}} ` , but the later conversation says ` OldTest . js ` was deleted and final verification ran ` NewTest ` −> omit ` OldTest . js ` and keep ` test − runner NewTest `. Observed test commands / tool args : ``` { observed_test_commands } ``` Conversation : ``` { conversation_context } ```

Prompt A.5 – Runtime Instruction Wrapper

The instruction wrapper an implementer agent receives at runtime to regenerate code from a specification and satisfy its verification conditions. You are given a ∗∗ Re im pl em en ta ti on Spec ∗∗ — a r e i m p l e m e n t a t i o n specification plus a ,→ verification checklist that describes what changes need to be made to this codebase . ,→ Your task is to implement code changes that satisfy the specification and ALL of its ,→ verification conditions . ## R e i m p l e m en ta tio n Spec { spec } ## Instructions

23

1. Read the spec carefully − focus on the ∗∗ Intent and Rationale ∗∗ , ∗∗ Essential Design ,→ Decisions ∗∗ , ∗∗ Undi scoverable Facts ∗∗ , and the ∗∗ Verification Conditions ∗∗ checklist 2. Explore the codebase to understand the current state 3. Implement code changes that satisfy the spec and answer YES to every verification ,→ condition 4. The spec describes WHAT should change , not HOW to implement it − use your judgment ,→ for implementation details 5. Do NOT over − engineer − make the minimal changes needed to satisfy the spec and its ,→ verification conditions

A.2

Multi-Tier Verification Graders

Three graders evaluate regenerated code C ′ against the reference change C and combine into a single weighted score, solve_score = 3 · flex + 2 · vc + 1 · align (maximum 6.0). Each continuous grader emits its grade as a final FINAL_GRADE=<ratio> line; the ground-truth grader is binary. Tier labels below follow the grader source files, which number the ground-truth tier first—the reverse of the paper’s ordering. Prompt A.6 – Flexible Test-Execution Grader (Tier 3)

Runs the extracted test manifest against C ′ and reports a continuous pass ratio in [0, 1]. You are an execution verification grader . You run a provided test manifest against ,→ generated code C ' and may salvage tests only when failures are structural ,→ mismatches . You report a continuous PASS RATIO in [0.0 , 1.0] ( the fraction of ,→ runnable tests that pass ) , not a binary pass / fail verdict . This ratio feeds the ,→ solve_score aggregator . Test Manifest ( JSON array ) : { test_manifest } Max Salvage Attempts : { m a x _ s a l v a g e _ a t t e m p t s } Diff Number : { diff_number } Repository Type : { re posi tory _ty pe } Repository Path : { re posi tory _pa th } Instructions : − Parse test_manifest as a JSON array of objects with command and category fields . ,→ category is " new " or " regression ". − If the manifest is empty or invalid , call s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l with ,→ pass = false and grade =0.0 and the reason " no runnable tests ". − Run each command exactly as provided from the repository root , or from ,→ r ep os i tory _pat h for git repositories . − If a test fails because of import paths , symbol names , module names , or ,→ constructor / function signatures , you may adapt the test harness and rerun . − You may adapt imports , module names , function / class names , and signatures only . − You must not adapt assertions , expected values , or behavioral checks . − Never modify im plementation code . − If a test command references a test method or class that does not exist , inspect the ,→ original / reference patch C by running the version control system ' s diff command for ,→ the reference change { diff_number } via ex ec u te _c om ma n d . − Mark a missing test as SKIPPED only when the original / reference patch C removed or ,→ renamed that test , or removed the feature / behavior that the test covered . Use the ,→ reason " test intentionally removed by reference patch ". Do not count it as a failure . − If the reference patch does not remove or rename the missing test / covered behavior , ,→ or if the evidence is inconclusive , mark the command as FAIL . Do not skip solely ,→ because the generated checkout lacks the test . − Stop after m a x _ s a l v a g e _ a t t e m p t s total adaptations . − Compute passed_ratio = passing tests / ( total tests − skipped tests ) , the fraction of ,→ runnable tests that pass after allowed salvage , a float in [0.0 , 1.0]. Report the ,→ exact ratio ( e . g . 0.5 for 1 of 2) — do NOT round to 0 or 1. If every test is SKIPPED ,→ so there are no runnable tests , set passed_ratio =0.0.

24

− REQUIRED FINAL STEP : call s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l exactly once with ,→ grade = passed_ratio ( the numeric ratio ) and pass = true only if all regression tests ,→ pass ( excluding skipped ) and every runnable new test passes after allowed salvage , ,→ otherwise pass = false . The grade carries the continuous signal consumed by the ,→ solve_score aggregator ; the pass flag is only a coarse indicator and is NOT used in ,→ the score . − Wait for the s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l response before writing your final verdict . − REQUIRED : the VERY LAST line of your exit report must be a single machine − readable ,→ marker in EXACTLY this format , with no other text on the line : ,→ ` FINAL_GRADE = < passed_ratio > ` where < passed_ratio > is the numeric ratio as a decimal ,→ in [0.0 , 1.0] ( e . g . ` FINAL_GRADE =0.5 `) . Emit it on every path , including when there ,→ are no runnable tests ( use ` FINAL_GRADE =0.0 `) . This line is parsed by the optimizer ,→ and must always be present and exact . − Exit with the report below . < format > # Flex Test Verdict ## Test Results | Command | Category | Result | Adaptations | Evidence | | − − − − − − − − −| − − − − − − − − − −| − − − − − − − −| − − − − − − − − − − − − −| − − − − − − − − − −| | [ cmd ] | [ new / regression ] | [ PASS / FAIL / SKIPPED ] | [ none or summary ] | [ log excerpt ,→ or reason for skip ] | ## Summary total : [ N ] passed : [ N ] skipped : [ N ] passed_ratio : [0.0 −1.0] ( passing / ( total − skipped ) ) ,→ grade new_p ercentage : [0.0 −1.0 or N / A ] r e g r e s s i o n _ p e r c e n t a g e : [0.0 −1.0 or N / A ]

−− this value is reported as

## Result passed_ratio =[0.0 −1.0] −− [ Pass / Fail ] </ format >

Prompt A.7 – Verifiable-Condition Check Grader (Tier 2)

Checks how many of the extracted verification conditions C ′ satisfies and reports a continuous ratio in [0, 1]. You are an intent − level verification grader . You check whether generated code C ' ,→ satisfies concrete verification clues extracted from the source conversation . You ,→ report a continuous satisfaction RATIO in [0.0 , 1.0] ( the fraction of evaluable ,→ clues that C ' satisfies ) , not a binary pass / fail verdict . This ratio feeds the ,→ solve_score aggregator . Verification Clues ( JSON array of unique clue strings ) : { v e r i f i c a t i o n _ c l u e s } Pass Threshold : { pass_thresh old } Repository Type : { re posi tory _ty pe } Repository Path : { re posi tory _pa th } Instructions : − Parse v er i f i ca t i o n_ c l u e s as a JSON array of unique clue strings . If it is invalid , ,→ call s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l with pass = false and grade =0.0 and a clear reason . − If v e r i f ic a t i on _ c l ue s is an empty array , do not inspect the diff . Record a SKIP by ,→ calling s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l with pass = true and grade =0.0 and summary ,→ " SKIP : no verification clues to evaluate " , then exit with a report that has ,→ passed =0 , failed =0 , skipped =0 , total =0 , sa ti sf i ed _r at i o =0.0 ( N / A ) , and Result = Skip . − Use c h e c k _ c h a n g e s _ s i n c e _ l a s t _ c o m m i t to inspect generated changes C '. − For each clue , read the relevant source files and decide PASS or FAIL . − Cite file : line evidence when possible ; use " not found " evidence for failures .

25

− IMPORTANT : Your scope is the behavioral correctness of the code diff . Do NOT evaluate : − Test existence or test coverage — whether tests were added or updated is handled by ,→ the test − execution grader . − Test execution outcomes — whether tests pass is handled by the test − execution ,→ grader . − External system state — feature − flag config , config − service metadata , spreadsheet ,→ data , dashboard data . If a clue falls into these categories , mark it SKIP and exclude it from the satisfied ,→ ratio . − Compute sa tisf ied _rat io = passed clues / ( total clues − skipped clues ) . This is the ,→ fraction of evaluable verification clues satisfied by C ' , a float in [0.0 , 1.0]. ,→ Report the exact ratio ( e . g . 0.6667 for 2 of 3) — do NOT round to 0 or 1. − If every clue is SKIP and there are no evaluable clues , record a SKIP by calling ,→ s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l with pass = true and grade =0.0 and summary " SKIP : no ,→ evaluable verification clues " , then exit with Result = Skip . Do not mark all − skipped ,→ clue sets as Fail . − REQUIRED FINAL STEP : call s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l exactly once with ,→ grade = sa tisf ied_ rat io ( the numeric ratio ) and pass = true when sa t is fi ed _ ra ti o is at ,→ least pass_threshold , otherwise pass = false . The grade carries the continuous signal ,→ consumed by the solve_score aggregator ; the pass flag is only a coarse threshold ,→ indicator and is NOT used in the score . − Wait for the s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l response before writing your final verdict . − Do not finish , exit , or claim the grading result was recorded until ,→ s e t _ f l o a t _ g r a d i n g _ r e s u l t _ t o o l has returned successfully . − REQUIRED : the VERY LAST line of your exit report must be a single machine − readable ,→ marker in EXACTLY this format , with no other text on the line : ,→ ` FINAL_GRADE = < satisfied_ratio > ` where < satisfied_ratio > is the numeric ratio as a ,→ decimal in [0.0 , 1.0] ( e . g . ` FINAL_GRADE =0.6667 `) . Emit it on every path , including ,→ SKIP ( use ` FINAL_GRADE =0.0 `) . This line is parsed by the optimizer and must always ,→ be present and exact . − Exit with the JSON − like report below . < format > # Verification Clues Verdict ## Clue Results | Clue | Result | Evidence | | − − − − − −| − − − − − − − −| − − − − − − − − − −| | [ full clue ] | [ PASS / FAIL / SKIP ] | [ file : line or not found or reason for skip ] | ## Overall passed : [ N ] failed : [ N ] skipped : [ N ] total : [ N ] s at is fi e d_ra tio : [0.0 −1.0] ( passed / ( total − skipped ) ) ,→ grade

−− this value is reported as

## Result s at is fi e d_ra tio =[0.0 −1.0] −− pass_thresh old =[ value ] −− [ Pass / Fail ] FINAL_GRADE =[0.0 −1.0] </ format >

Prompt A.8 – Ground-Truth Alignment Grader (Tier 1)

Issues a binary Pass/Fail behavioral-equivalence verdict comparing C ′ against the reference change C. You are an expert code verifier . You verify whether generated code C ' is behaviorally ,→ equivalent to the reference change C for the stated specification , modulo the source ,→ conversation context when it is provided . Task Description : { ta sk _d es cr ip ti on }

26

Specification : { s pe c_ de sc rip ti on } Conversation Context : { c o n v e r s a t i o n _ c o n t e x t } Repository Type : { re posi tory _ty pe } Repository Path : { re posi tory _pa th } Reference Patch Available : { h a s _ re f e r e n c e _ p a t c h } Instructions : − Read the task description , optional specification description , and optional ,→ conversation context . − Use c h e c k _ c h a n g e s _ s i n c e _ l a s t _ c o m m i t to inspect generated changes C '. − If a reference patch is available , use g e t _ r e f e r e n c e _ p a t c h to inspect C . − Read relevant source files before making behavioral claims . − Trace concrete scenarios and actively look for evidence against your conclusion . − REQUIRED FINAL STEP ( do this exactly once , and BEFORE you call exit ) : call ,→ s e t _ g r a d i n g _ r e s u l t _ t o o l with pass = true when C ' is behaviorally equivalent to C ( your ,→ verdict is Pass ) or pass = false otherwise ( Fail ) . The boolean you pass MUST match the ,→ "## Result " line of your verdict below . − Do NOT call exit until s e t _ g r a d i n g _ r e s u l t _ t o o l has been called . If you have already ,→ written your verdict text , still call s e t _ g r a d i n g _ r e s u l t _ t o o l first — a verdict that ,→ is not recorded through s e t _ g r a d i n g _ r e s u l t _ t o o l is counted as a Fail regardless of ,→ your written conclusion , so you must always emit it . Emit it even when you are ,→ highly confident or when the answer seems obvious . − Only after s e t _ g r a d i n g _ r e s u l t _ t o o l succeeds , call exit and include the structured ,→ reasoning trace below ( its "## Result " must agree with the pass value you sent ) . < format > # Verification Verdict ## Issue / Change Summary [2 −3 sentence summary ] ## Function Trace Table | Function / Method | File : Line | Behavior ( VERIFIED ) | | − − − − − − − − − − − − − − − − −| − − − − − − − − − − −| − − − − − − − − − − − − − − − − − − − − −| | [ function ] | [ file : N ] | [ actual behavior ] | ## Behavioral Comparison [ Concrete scenarios comparing C and C '] ## Conversation Alignment [ How the verdict accounts for provided conversation context , or " No conversation ,→ context provided "] ## Alternative Hypothesis Check [ Evidence searched for and found ] ## Critical Differences [ Behavioral issues or " None identified "] ## Result [ Pass / Fail ] −− Confidence : [ HIGH / MEDIUM / LOW ] </ format >

27