Agentic Synthesis against Counterexample-Supplemented Sketches

Eric Rubeck; Muness Castle

REVIEW 3 major objections 4 minor 23 references

This paper argues that agent-driven code synthesis can preserve domain policy if every approved counterexample revises a human-readable sketch, and the workflow advances only after a deterministic replay/compare gate and a separate review a

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-04 04:11 UTC pith:RV5P2BVP

load-bearing objection An honest, well-scoped methodology paper whose real contribution is procedural, but whose headline empirical claim rests on a single unblinded run and is statistically indistinguishable from noise. the 3 major comments →

arxiv 2607.15854 v2 pith:RV5P2BVP submitted 2026-07-17 cs.SE cs.AI

Agentic Synthesis against Counterexample-Supplemented Sketches

Muness Castle , Eric Rubeck This is my paper

classification cs.SE cs.AI

keywords counterexamplesketchagentic codingpolicy preservationregression gateapproved-output comparereplayCatSynth

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Coding agents can fix a failing test without preserving the domain rule that caused the failure, and ordinary regression tests cannot see the difference. This paper proposes a repository-native loop: every accepted counterexample must be explicitly approved by an operator, change a human-readable sketch of the policy, and then survive both a deterministic replay-plus-approved-output gate and a separate review of the simulated outputs against the sketch. If true, this makes the learned policy inspectable and re-derivable: the implementation can be discarded and regenerated from the sketch. On a captured synthetic suite, the reviewed sketch carried three more withheld cases than raw example replay, while retained code did not beat clean regeneration. The claim is deliberately bounded to the selected cases, checkers, and review records.

Core claim

The central discovery is that a repair loop which treats a rejected repair as a reviewed change to the governing model—not as a one-off patch—preserves the rule the repair was meant to obey. The paper defines a workflow where an SME correction becomes a counterexample only after explicit operator approval; every accepted counterexample revises the sketch S; and the workflow advances only after both the deterministic gate (replay plus approved-output compare over the regression set R) and a separate review of simulated outputs against S pass. Theorem 1 formalizes the finite-regression part: if the gate passes for a strategy H and regression set R, then H is R-correct with respect to the encod

What carries the argument

The load-bearing mechanism is the counterexample-supplemented sketch S: a reviewable, agent-editable artifact recording the strategy space, policy ordering, holes, anchors, and forbidden repairs, which must change with every accepted counterexample. Around it sits the two-check gate: a deterministic replay predicate (does the output close the encoded state gap?) plus an approved-output compare predicate (does the output match the approved policy-bearing fields?), followed by a separate sketch review in which a capable model or person judges the simulated outputs against the full sketch clause. The sketch's role is to carry learned policy so the implementation can be discarded and regenerated

Load-bearing premise

The second check only adds value if a model or person reviewing simulated outputs against the current sketch can reliably distinguish genuine policy violations from implementation defects; the paper acknowledges reviewers can misread the sketch, share the implementation's blind spots, or judge inconsistently.

What would settle it

Run the two-check protocol with a sketch intentionally missing one withheld rule, and give the reviewer no access to that rule; if the second check still passes violating outputs at the same rate as raw replay, the claimed advantage of the reviewed sketch disappears. More directly, exhibit any single case outside R where the gate and sketch review both pass but the output violates the operator-approved policy—that falsifies the bounded claim as stated.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

A passing gate yields a bounded invariant: for the current regression set, replay checker, comparer, and approved rows, the strategy is R-correct (Theorem 1).
Every accepted counterexample must change the sketch; a passing proposal is coverage, not a counterexample.
No new candidate is revealed until both the gate and sketch review pass for the active case and the curated regression set.
Periodic clean regeneration from sketch and anchors tests whether the sketch, not retained implementation history, carries the learned policy.
In the CatSynth two-check rerun, the reviewed sketch passed three more withheld cases than raw example replay (17 vs 14 of 21), while retained code did not beat clean regeneration.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

If this loop scales, the bottleneck in agentic coding shifts from test coverage to policy encoding: a human-readable sketch that changes only through approved counterexamples could act as a durable contract between subject-matter experts and agents.
Separating replay from approved-output compare predicts a failure class a combined assertion would hide: repairs that close the state gap while choosing the wrong operation; suites reporting only aggregate pass/fail would not surface this distinction.
The sketch-review step makes reviewer attention the real cost, so an automated reviewer could become the weak link; a testable extension is measuring inter-reviewer agreement on sketch-review verdicts.
CatSynth's R=A is an experiment choice, not the method; a scaled version needs a curation policy, and the paper does not specify one beyond 'distinct boundaries.'

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

An honest, well-scoped methodology paper whose real contribution is procedural, but whose headline empirical claim rests on a single unblinded run and is statistically indistinguishable from noise.

read the letter

Dear [Colleague],

The paper addresses a real problem: coding agents that pass tests while violating unstated domain rules. Its contribution is procedural, not formal: making the sketch a first-class, operator-approved artifact, requiring both a deterministic gate and separate sketch review before revealing the next candidate. That combination is new and the paper is refreshingly honest about its boundaries.

What it does well: the workflow is clearly specified, the artifact definitions are sensible, and the CatSynth capture is reproducible in principle. The authors explicitly disclaim the earlier 19/21 result for lacking sketch review, and Theorem 1 is correctly scoped to what the gate checks. The discussion of double-loop learning is fair and not overstated.

The soft spots are real and load-bearing. Theorem 1 is definitional, not an empirical result. The empirical evidence is one stochastic run per path with one model and one reveal order. The 17 vs 14 withheld-case difference is within binomial noise (sd roughly 2 cases), so the "three more withheld cases" headline is not statistically meaningful. More importantly, the distinguishing feature—sketch review—is exactly the part that is not validated. The A.16 continuation used manual review by the authors, who had designed the frozen withheld cases; that risks reviewer knowledge steering the sketch toward the withheld answers. The paper itself concedes (Limitation 7) that reviewers can misread the sketch or share blind spots, and (Limitation 9) that the original capture does not measure the review step. So the central advantage is asserted on evidence that cannot support it.

None of this is hidden. The authors are transparent about the single-run, single-model limitation and explicitly bound their claims. The method is a plausible engineering contribution; it just needs a multi-seed evaluation and a blinded or independent review protocol before the empirical claim carries weight.

This paper is for teams building agentic coding workflows where policy is discovered during implementation, and for researchers interested in how synthesis ideas transfer to repository practice. It deserves serious peer review, but with the expectation of substantial revision—not acceptance as is. I would bring it to a reading group, but I would not cite the empirical claim in my own work.

Recommendation: send to peer review, but the referees should focus on whether the review step can be shown to cause the claimed improvement rather than reviewer knowledge or luck.

Referee Report

3 major / 4 minor

Summary. The paper proposes Sketch-CE, a repository-native workflow for agentic code synthesis in settings where domain policy is discovered incrementally. A human provides a partial sketch; a coding agent generates a replaceable implementation. When simulation exposes a policy gap, an operator approves the corrected behavior and the minimum general rule it authorizes, and every accepted counterexample must revise the sketch. Before the next candidate is revealed, the workflow requires both a deterministic gate (replay plus approved-output comparison over the active case and the regression set) and a separate human/model review of the simulated outputs against the current sketch. The formal claim is Theorem 1: if the gate passes for a strategy on regression set R, the strategy is R-correct with respect to the encoded replay and compare predicates. The empirical part is a GPT-5.4-mini run on CatSynth, where all three variants pass 8/8 visible accepted cases and pass 14/21, 17/21, and 16/21 withheld cases for replay-all, evolved-sketch rebuild, and retained Sketch-CE respectively. The paper characterizes the reviewed sketch's 17-vs-14 withheld advantage as evidence that the second check helps, while acknowledging that one model and one reveal order cannot establish general superiority.

Significance. The paper addresses a genuinely important problem: agent patches can pass tests while violating domain rules that live only in the human's or reviewer's memory. The proposed separation of replay from approved-output comparison, the requirement that every accepted counterexample change the sketch, and the emphasis on provenance are practical and clearly presented. The attached audit trail — frozen candidates, per-generation directories, source maps, and reproduction commands — is unusually transparent and a real strength. The formal theorem is, however, deliberately weak: it is essentially a restatement of the gate definition and provides no formal support for the sketch-review step, which is the method's distinguishing feature. The paper is honest about this limitation. The central empirical claim — that sketch review produces a meaningful withheld-case advantage — is not yet established, because the evidence is a single unseeded run with manual reviewers who were not reported to be blind to the withheld cases. If the authors reframe the empirical component as an illustrative case study or add proper experimental controls, the contribution is publishable; in its current form, the a

major comments (3)

[A.16; Abstract] The headline claim that the reviewed sketch 'passed three more withheld cases than raw example replay' rests on a single unseeded run per condition. With 21 withheld cases and observed pass rates near 70%, the binomial standard deviation is roughly 2.1 cases, so the 17-vs-14 gap (and the 16 for retained code) is within one standard deviation of chance. No seeds, confidence intervals, or repeated runs are reported. The paper's own limitation 10 says 'one stochastic run per path,' but the Abstract still presents the comparison as a finding. Please provide a properly seeded/repeated evaluation, or explicitly label this difference as anecdotal rather than evidential.
[A.16; §10.5] The corrected two-check continuation is the central evidence that sketch review 'exposed drift' and produced the current 17/21 result. The appendix does not state who performed the manual sketch review or whether they were blind to the 21 withheld cases and authoritative expected outputs. Since the same investigators froze the candidate manifest and expected outputs before execution, reviewer knowledge of the withheld cases could have steered sketch revisions toward those cases. No review logs, adjudication records, or independent-reviewer statement are provided. Without blinding or reviewer independence, this run cannot distinguish the review mechanism from the reviewers' knowledge. Please add a blinding protocol, independent reviewers, or clearly demote the result to a demonstration of procedure rather than an effect estimate.
[§10.5; A.20] The paper is internally inconsistent about what the reported run measures. §10.5 says the captured results 'do not evaluate the added sketch-review requirement or its cost,' and A.1 says the capture 'predates the explicit requirement to record a separate post-repair sketch review.' Yet §10.5 and A.16 present the August 2 continuation as a 'corrected two-check' rerun with 'separate review of each simulated output against the current sketch' and use its withheld scores as the current result. A.20 then states 'The capture also does not evaluate the method's separate sketch-review step.' These statements cannot all hold. The authors should clarify which run is the official evaluation and, if the continuation is claimed to evaluate sketch review, provide the per-cycle review records and the exact protocol followed.

minor comments (4)

[A.12; §10.5] The generation labels and CE numbers are inconsistent: Generation 007 is referred to as CE10 and Generation 008 as CE12, while the running list in §10.5 labels them CE7 and CE8. Align the numbering to avoid confusion when tracing the archive.
[§10.5] The sentence 'Its final visible and withheld scores are reported below' refers to material that actually appears in A.16, not immediately below. Either move the table to §10.5 or add an explicit cross-reference.
[Section 9] Theorem 1 is correct but definitional: it unpacks Definition 10 and the two lemmas restate the encodings. This is acceptable as a bounded invariant, but calling it a 'soundness theorem' may overstate the formality. Consider renaming it to 'Finite-regression invariant' and moving the proof to a remark.
[A.20] The claim that 'adjudicated reviewer errors did not become policy' is not backed by any artifact reference. If such adjudication records exist, name the files; otherwise present this as an assertion rather than an observed outcome.

Circularity Check

0 steps flagged

No meaningful circularity: the formal gate theorem is a transparent definition-unpacking, the withheld-case advantage is not forced by construction, and there is no load-bearing self-citation chain.

full rationale

The paper's derivation chain is self-contained and explicitly bounded. Theorem 1 (Section 9) does reduce to the definitions: Gate pass (Definition 10) and R-correctness (Definition 11) are essentially the same conjunction over R, and the proof expands those definitions. But the paper openly labels this a finite-regression theorem over the current replay/compare code and approved rows, and it never uses the theorem to claim predictive power over withheld cases; that transparency means the theorem is a declared formal boundary, not a hidden circularity. The empirical claim that the reviewed sketch passed 17/21 versus 14/21 withheld cases is not guaranteed by construction: the withheld cases were frozen before the run, the evolved sketch was built from accepted/visible counterexamples, and the three paths (replay-all, evolved-sketch rebuild, retained Sketch-CE) are separate regeneration strategies rather than the same fitted artifact evaluated on its own training data. The paper cites external prior work (Solar-Lezama, CEGIS, SWE-bench, FlashMeta, etc.) and does not rest its central premise on a self-citation chain. The acknowledged limitations—Limitation 7 (a reviewer can misread the sketch or share blind spots), Limitation 9 (the original capture did not record separate sketch review), and Limitation 10 (one stochastic run per path, no causal estimate)—are validity threats about reviewer reliability and single-run noise, not reductions of the claimed result to its inputs. Even if the unblinded manual review could weaken the empirical inference, that is an experimental-control concern, not circularity by construction.

Axiom & Free-Parameter Ledger

4 free parameters · 5 axioms · 0 invented entities

The paper introduces no new physical or mathematical objects; the 'sketch', 'counterexample archive', and 'dual gate' are workflow artifacts. The ledger shows the central claim rests on human judgment and the assumption that the protocol's components behave as intended. The free parameters are the case selection, sketch design, and model/order choices.

free parameters (4)

Regression set R size/composition = 8 cases (R=A)
The choice of which cases enter R is made by maintainers and directly affects the gate's guarantees. The paper notes this is an experiment choice. The theorem covers only R, so the empirical result is tied to this specific set.
Sketch design / initial policy rules = initial_sketch.md
The initial CatSynth sketch fixes preference weights, ordinal maps, and policy surfaces. The withheld-case advantage depends on how well this sketch captures the domain before discovery; it is a human-selected input, not derived.
Model, candidate order, and reveal order = GPT-5.4-mini, 14 candidates
The paper explicitly states this is one model and one reveal order. The experimental results are conditional on these choices.
Oracle prompt and code implementation choices = generated by GPT-5.4-mini
The implementation details affect which withheld cases pass or fail, but the paper treats them as replaceable surfaces. The model's stochastic choices are a significant source of variance.

axioms (5)

domain assumption Gate semantics are correctly implemented in the repository
Theorem 1 relies on replay and approved-output compare faithfully encoding the intended state-repair and policy-field checks. The paper acknowledges a buggy checker can certify wrong behavior (Limitation 2). This is an unverified assumption about the implementation.
domain assumption The SME/operator correctly identifies the authoritative corrected output and the minimum general rule
The entire workflow depends on human judgment being correct at the approval step. Limitations 3 and 4 note a wrong golden row or approval can corrupt the policy. This assumption is not proved and is in fact recognized as a risk.
domain assumption The reviewer (model or person) can reliably judge whether a simulated output follows the current sketch
The sketch-review step is load-bearing for the two-check claim. Limitation 7 admits reviewers can misread the sketch or share blind spots. The empirical advantage is therefore conditional on reliable review, which is not independently established.
domain assumption The agent Developer will not silently change policy without operator approval
The protocol requires Developer to revise the sketch only when authorized, but the implementation is a stochastic LLM with prompt-level constraints. The paper itself notes the protocol fails if Developer rewrites the sketch to justify its patch. This is a strong assumption about model behavior.
domain assumption Natural-language sketches can be interpreted deterministically enough for review
The method relies on prose sketches and review against them. This is an unproven assumption that varies with the model and the sketch; the paper's bounded claims are tied to this assumption.

pith-pipeline@v1.3.0-alltime-deepseek · 19615 in / 7535 out tokens · 60627 ms · 2026-08-04T04:11:53.607077+00:00 · methodology

0 comments

read the original abstract

Coding agents can fix a failing example without preserving the domain rule that made it fail. We present agentic synthesis against counterexample-supplemented sketches, a repository-native method for systems whose policy is discovered during implementation. A human starts with a partial sketch, and a coding agent compiles a replaceable projection. When simulation exposes missing or mistaken policy, an operator approves the corrected behavior and the minimum general rule the case authorizes. Every Developer call names its change authority and the rules, holes, anchors, and approved behavior that must survive. Conflict or ambiguous permission leaves the files unchanged and produces a clarification question. A complete archive preserves provenance; a curated regression set gates distinct boundaries. Before another candidate is revealed, the active case and curated regressions must pass both deterministic approved-output comparison and a separate review against the current sketch. Periodic clean regeneration tests whether the sketch carries the learned policy. We demonstrate the method with CatSynth, a captured synthetic application. In one open-world run with GPT-5.4-mini, 8 of 14 frozen candidates became counterexamples. Under the corrected protocol, replay-all, evolved-sketch rebuild, and retained Sketch-CE each passed all 8 accepted cases. They passed 14, 17, and 16 of 21 withheld cases, respectively. Sketch review rejected premature empty-input and tag policies and restored dropped anchors; adjudicated reviewer errors did not become policy. One model and one reveal order cannot establish general correctness or superiority. On this suite, the second check exposed drift hidden by deterministic replay, and the reviewed sketch passed three more withheld cases than raw example replay.

Review history (2 revisions) →

discussion (0)

Reference graph

Works this paper leans on

23 extracted references · 1 linked inside Pith

[1]

Manning Publications, 2011

Gojko Adzic.Specification by Example: How Successful Teams Deliver the Right Software. Manning Publications, 2011

2011
[2]

Double loop learning in organizations.Harvard Business Review, 55(5):115–125, 1977

Chris Argyris. Double loop learning in organizations.Harvard Business Review, 55(5):115–125, 1977

1977
[3]

Natural language-oriented programming (NLOP): Towards democratizing software creation

Amin Beheshti. Natural language-oriented programming (NLOP): Towards democratizing software creation. In2024 IEEE International Conference on Software Services Engineering, SSE 2024, pages 258–267. IEEE, 2024

2024
[4]

Zhang, and Yang Liu

Zhenpeng Chen, Chong Wang, Weisong Sun, Xuanzhe Liu, Jie M. Zhang, and Yang Liu. Promptware engineering: Software engineering for prompt-enabled systems, 2025

2025
[5]

Tests as prompt: A test-driven-development benchmark for llm code generation, 2025

Yi Cui. Tests as prompt: A test-driven-development benchmark for llm code generation, 2025

2025
[6]

Github copilot workspace: Welcome to the copilot-native developer environment

Thomas Dohmke. Github copilot workspace: Welcome to the copilot-native developer environment. GitHub Blog, 2024. Published April 29, 2024

2024
[7]

What is spec-driven development? GitHub Spec Kit Documentation, 2026

GitHub. What is spec-driven development? GitHub Spec Kit Documentation, 2026. Accessed July 1, 2026

2026
[8]

Program synthesis.Foundations and Trends in Programming Languages, 4(1–2):1–119, 2017

Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program synthesis.Foundations and Trends in Programming Languages, 4(1–2):1–119, 2017

2017
[9]

Seshia, and Ashish Tiwari

Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. Oracle-guided component-based program synthesis. InProceedings of the 32nd ACM/IEEE International Conference on Software En- gineering, ICSE 2010, pages 215–224, 2010

2010
[10]

Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R

Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R. Narasimhan. SWE-bench: Can language models resolve real-world github issues? InThe Twelfth International Conference on Learning Representations, 2024. 23

2024
[11]

Andrew J. Ko, Robin Abraham, Laura Beckwith, Alan Blackwell, Margaret Burnett, Martin Erwig, Chris Scaffidi, Joseph Lawrance, Henry Lieberman, Brad Myers, Mary Beth Rosson, Gregg Rothermel, Mary Shaw, and Susan Wiedenbeck. The state of the art in end-user software engineering.ACM Computing Surveys, 43(3), 2011

2011
[12]

Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing.ACM Computing Surveys, 55(9):1–35, 2023

Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig. Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing.ACM Computing Surveys, 55(9):1–35, 2023

2023
[13]

Flashmeta: A framework for inductive program synthesis

Oleksandr Polozov and Sumit Gulwani. Flashmeta: A framework for inductive program synthesis. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pages 107–126. ACM, 2015

2015
[14]

Prompt programming for large language models: Beyond the few-shot paradigm.arXiv preprint arXiv:2102.07350, 2021

Laria Reynolds and Kyle McDonell. Prompt programming for large language models: Beyond the few-shot paradigm.arXiv preprint arXiv:2102.07350, 2021

Pith/arXiv arXiv 2021
[15]

PhD thesis, EECS Department, University of California, Berkeley, December 2008

Armando Solar Lezama.Program Synthesis by Sketching. PhD thesis, EECS Department, University of California, Berkeley, December 2008

2008
[16]

Program sketching.International Journal on Software Tools for Technology Transfer, 15(5–6):475–495, 2013

Armando Solar-Lezama. Program sketching.International Journal on Software Tools for Technology Transfer, 15(5–6):475–495, 2013

2013
[17]

Seshia, and Vijay A

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit A. Seshia, and Vijay A. Saraswat. Com- binatorial sketching for finite programs. InProceedings of the 12th International Conference on Ar- chitectural Support for Programming Languages and Operating Systems, ASPLOS 2006, pages 404–415. ACM Press, 2006

2006
[18]

Introducing kiro

Nikhil Swaminathan and Deepak Singh. Introducing kiro. Kiro Blog, 2025. Published July 14, 2025. 24 A CatSynth Artifact Supplement This is the audit and reproduction companion toAgentic Synthesis against Counterexample- Supplemented Sketches. The paper contains the complete argument, method, experimental design, reported results, and limitations. The dist...

2025
[19]

Which single failure was visible to each Developer generation?
[20]

How did the sketch, deterministic code, and prompt change together?
[21]

How did every accepted CE change the sketch?
[22]

Which regression gate ran after each revision?
[23]

semantic compare,

Which proposed cases became accepted CEs, and which were recorded only as coverage? A.15 The open-world comparison The conceptual contrast remains spec-first versus Sketch-CE: a complete specification works when the problem is already known, while Sketch-CE changes the governing sketch as the world reveals new policy. The captured open-world experiment ad...

2026

[1] [1]

Manning Publications, 2011

Gojko Adzic.Specification by Example: How Successful Teams Deliver the Right Software. Manning Publications, 2011

2011

[2] [2]

Double loop learning in organizations.Harvard Business Review, 55(5):115–125, 1977

Chris Argyris. Double loop learning in organizations.Harvard Business Review, 55(5):115–125, 1977

1977

[3] [3]

Natural language-oriented programming (NLOP): Towards democratizing software creation

Amin Beheshti. Natural language-oriented programming (NLOP): Towards democratizing software creation. In2024 IEEE International Conference on Software Services Engineering, SSE 2024, pages 258–267. IEEE, 2024

2024

[4] [4]

Zhang, and Yang Liu

Zhenpeng Chen, Chong Wang, Weisong Sun, Xuanzhe Liu, Jie M. Zhang, and Yang Liu. Promptware engineering: Software engineering for prompt-enabled systems, 2025

2025

[5] [5]

Tests as prompt: A test-driven-development benchmark for llm code generation, 2025

Yi Cui. Tests as prompt: A test-driven-development benchmark for llm code generation, 2025

2025

[6] [6]

Github copilot workspace: Welcome to the copilot-native developer environment

Thomas Dohmke. Github copilot workspace: Welcome to the copilot-native developer environment. GitHub Blog, 2024. Published April 29, 2024

2024

[7] [7]

What is spec-driven development? GitHub Spec Kit Documentation, 2026

GitHub. What is spec-driven development? GitHub Spec Kit Documentation, 2026. Accessed July 1, 2026

2026

[8] [8]

Program synthesis.Foundations and Trends in Programming Languages, 4(1–2):1–119, 2017

Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program synthesis.Foundations and Trends in Programming Languages, 4(1–2):1–119, 2017

2017

[9] [9]

Seshia, and Ashish Tiwari

Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. Oracle-guided component-based program synthesis. InProceedings of the 32nd ACM/IEEE International Conference on Software En- gineering, ICSE 2010, pages 215–224, 2010

2010

[10] [10]

Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R

Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R. Narasimhan. SWE-bench: Can language models resolve real-world github issues? InThe Twelfth International Conference on Learning Representations, 2024. 23

2024

[11] [11]

Andrew J. Ko, Robin Abraham, Laura Beckwith, Alan Blackwell, Margaret Burnett, Martin Erwig, Chris Scaffidi, Joseph Lawrance, Henry Lieberman, Brad Myers, Mary Beth Rosson, Gregg Rothermel, Mary Shaw, and Susan Wiedenbeck. The state of the art in end-user software engineering.ACM Computing Surveys, 43(3), 2011

2011

[12] [12]

Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing.ACM Computing Surveys, 55(9):1–35, 2023

Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig. Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing.ACM Computing Surveys, 55(9):1–35, 2023

2023

[13] [13]

Flashmeta: A framework for inductive program synthesis

Oleksandr Polozov and Sumit Gulwani. Flashmeta: A framework for inductive program synthesis. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pages 107–126. ACM, 2015

2015

[14] [14]

Prompt programming for large language models: Beyond the few-shot paradigm.arXiv preprint arXiv:2102.07350, 2021

Laria Reynolds and Kyle McDonell. Prompt programming for large language models: Beyond the few-shot paradigm.arXiv preprint arXiv:2102.07350, 2021

Pith/arXiv arXiv 2021

[15] [15]

PhD thesis, EECS Department, University of California, Berkeley, December 2008

Armando Solar Lezama.Program Synthesis by Sketching. PhD thesis, EECS Department, University of California, Berkeley, December 2008

2008

[16] [16]

Program sketching.International Journal on Software Tools for Technology Transfer, 15(5–6):475–495, 2013

Armando Solar-Lezama. Program sketching.International Journal on Software Tools for Technology Transfer, 15(5–6):475–495, 2013

2013

[17] [17]

Seshia, and Vijay A

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit A. Seshia, and Vijay A. Saraswat. Com- binatorial sketching for finite programs. InProceedings of the 12th International Conference on Ar- chitectural Support for Programming Languages and Operating Systems, ASPLOS 2006, pages 404–415. ACM Press, 2006

2006

[18] [18]

Introducing kiro

Nikhil Swaminathan and Deepak Singh. Introducing kiro. Kiro Blog, 2025. Published July 14, 2025. 24 A CatSynth Artifact Supplement This is the audit and reproduction companion toAgentic Synthesis against Counterexample- Supplemented Sketches. The paper contains the complete argument, method, experimental design, reported results, and limitations. The dist...

2025

[19] [19]

Which single failure was visible to each Developer generation?

[20] [20]

How did the sketch, deterministic code, and prompt change together?

[21] [21]

How did every accepted CE change the sketch?

[22] [22]

Which regression gate ran after each revision?

[23] [23]

semantic compare,

Which proposed cases became accepted CEs, and which were recorded only as coverage? A.15 The open-world comparison The conceptual contrast remains spec-first versus Sketch-CE: a complete specification works when the problem is already known, while Sketch-CE changes the governing sketch as the world reveals new policy. The captured open-world experiment ad...

2026