Skeleton Coding: Program Structure as a Specification for Agents

1 Introduction

• Test sufficiency depends on implementation structure, leaving developers unable to know whether their tests suffice without extensive testing or inspection of generated code.A test suite sufficient for one design may leave another badly underdetermined.Source: §1 · pp. 2–3
• Skeleton Coding specifies data types, module boundaries, function signatures, data flow, contracts, and invariants while leaving implementation to the agent.The authors propose jointly specifying structure and behavior as a control action.Source: §1 · p. 2
• Skeletons can reduce required tests exponentially by shrinking the hypothesis class, exposing intermediate state, and directly stating output-invisible requirements.For an n-function dataflow, local tests may identify it with O(n) tests, while end-to-end tests may need O(2n).Source: §1 · p. 3
• Formally verifiable contracts can address the lack of convergence guarantees from adding specifications iteratively, while an imperfect verifier can still speed convergence to a valid implementation.The paper distinguishes prompt-based steering from Bayesian conditioning.Source: §1 · p. 3
• A persistent skeleton records requirements and can help agents rewrite cleanly when functionality changes instead of accumulating patches that contribute to “AI code slop” [12].The paper also notes that teams can version, diff, review, and revise skeletons alongside implementations.Source: §1 · pp. 3–4

Empirical results.

• Structural specifications raise mean pass rate from 72% to 89% on SCBench [12] and from 29.0% to 74.2% on SDDBench, while behavioral specifications gain at most 9.4 percentage points.On ProgramBench [13], skeletons raise relative pass rate by 10.9% even with a full behavioral oracle.Source: Empirical results · p. 4
• With a detailed skeleton, a small model comes within 5–8 percentage points of the largest model’s pass rate at 15–26× lower implementation cost.The paper reports skeletons narrow the gap between small and large models.Source: Empirical results · p. 4
• Skeletons reduce code erosion by 24.7% on average where behavioral specifications increase it.Source: Empirical results · p. 4
• Code-like skeletons outperform prose design documents, and iterative repair reaches similar error rates with 32% fewer reference-executable queries.Source: Empirical results · p. 4

2 Controlling Coding Agents with Skeletons

• A skeleton specifies program architecture while leaving implementation to the agent, restricting its search to programs that share the specified structure.The developer’s goal is to produce a program in the acceptable set; behavioral tests select among programs within the skeleton’s hypothesis class.Source: §2 · pp. 4–5

2.1 Structure determines what tests are needed

• With equally large hypothesis classes, the choice of skeleton can change the number of tests needed exponentially, and tests designed for one skeleton may fail under another.Under one skeleton each test rules out at most one program, while under the other it rules out half of the incorrect programs; the theorem’s d-test suite can leave success probability 1/(2^d − d) under the first skeleton.Source: §2.1 · pp. 5–6, Figure 4 · p. 6

2.2 Interfaces make internal state observable

• Interfaces make intermediate state directly testable, avoiding the need for end-to-end tests to find inputs that expose errors before later computation masks them.For the stated transition-table setting, end-to-end testing requires 2^n tests, whereas 4n local tests suffice to identify the function.Source: §2.2 · pp. 6–7

2.3 Some requirements are invisible to output tests

• Behavioral tests cannot distinguish implementations with identical input-output behavior, so they cannot select among them based on requirements such as resource use or maintainability.The section reports that structural specifications reduce code erosion relative to the task-only condition, while behavioral specifications can increase it.Source: §2.3 · p. 7

2.4 What makes a good skeleton

• A good skeleton is short, gives components narrow interfaces and simple behaviors, and makes individually correct components compose into a globally correct program.Theorem 2.4 separates effort into skeleton description, local tests, and compatibility tests; complete Hoare-style contracts can eliminate compatibility tests, though they may lengthen the specification.Source: §2.4 · p. 8

3 Closing the Loop: Checks and Refinement

• Unlike Bayesian conditioning, prompting with additional specifications has no guarantee of convergence, and overly detailed contracts can lower pass rate.The prompted distribution may differ from the Bayesian posterior and may still violate the specification.Source: §3 · p. 9
• When specifications can be checked formally, rejection sampling can ensure convergence as specifications are added, at additional compute cost.With a skeleton and independently generated components, separate component checks can reduce the cost of rejection sampling.Source: §3 · p. 9
• Under the stated assumptions, resampling components separately takes a sum of inverse acceptance probabilities rather than the product required by whole-program resampling.Both procedures return programs distributed as the component proposal distribution conditioned on all components satisfying their contracts.Source: §3 · p. 9
• An informal judge makes an accepted component likely correct only when its error rate is much lower than the agent’s failure rate on that component.The informal contract’s literal allowances create a false-accept floor that even a perfect judge cannot remove; making the contract more precise can drive that floor to zero.Source: §3 · pp. 9–10

4 Empirical Results

• The experiments compare behavioral and structural specifications across greenfield applications, four models, and three benchmarks, measuring pass rate, code quality, and implementation cost.Structural conditions provide skeletons; behavioral conditions provide observations derived from a hidden reference code base, and the task-only baseline provides no specification.Source: §4 · pp. 10–11

4.1 Results

• Structural specifications reduce mean test error by 48.4% across four models, from 40.7% to 21.0%, compared with the best behavioral specifications.On SCBench and SDDBench, structural specifications raise mean pass rate from 71.7% to 89.2% and from 29% to 74.2%, respectively; behavioral specifications improve pass rate by at most 9.4 percentage points.Source: §4.1 · p. 11
• With oracle access on ProgramBench, adding a skeleton with local contracts raises mean pass rate 10.9% relative, from 64.0% to 70.9%.A skeleton with global invariants reduces mean test error by 27.0% relative, from 36.0% to 26.3%, versus the no-skeleton oracle setup; curated behavioral observations up to 160 still underperform a skeleton with 20 observations.Source: Figure 6 · p. 11, §4.1 · p. 12
• Adding architectural information raises pass rates, but 4–7× larger architecture specifications remain below the best code-like specifications on the same repositories.Pass rate rises from 61% to 71% on SCBench and from 40.1% to 52.8% on SDDBench as architectural information increases.Source: Figure 6 · p. 11, §4.1 · p. 12
• Adding correct but overly detailed local and global contracts to the best skeleton reduces performance, especially on smaller models.The authors note that prompting with added specifications need not approximate Bayesian conditioning, even though additional specifications should only improve the Bayesian posterior.Source: §4.1 · p. 13
• Signature specifications reduce code erosion from 0.66 to 0.56 on SCBench and from 0.41 to 0.24 on SDDBench, while behavioral specifications raise it to as much as 0.73 and 0.43.Verbosity varies less across conditions and is also lowest under structural specifications on SDDBench.Source: Figure 7 · p. 12, §4.1 · p. 13
• By repair round 8, the skeleton workflow reaches similar error rates with 32% fewer reference-binary calls, lower mean erosion, and higher mean maintainability.The study treats calls to the reference binary as a proxy for behavioral clarification effort.Source: §4.1 · p. 13, Figure 8 · p. 13

Contracts and formal specifications

• Program-logic and design-by-contract methods make interfaces, preconditions, postconditions, and invariants explicit; evaluated skeletons range from typed stubs to stubs with local contracts and global invariants.The evaluated contracts are not machine-checked; the study measures how much each contract component helps coding agents.Source: §5 · p. 13

Intermediate artifacts for code generation

• Prior intermediate-artifact workflows use plans, planning graphs, specifications, or tests, while this study varies skeleton contract content with the task and model held fixed.This separates skeleton content from artifact format and raw length.Source: §5 · p. 14

Specification-driven development

• Related specification-driven work includes modular design documents, structured pseudocode and module-level inputs, and separating specification elicitation from implementation.This paper complements those approaches by varying structural information in skeletons and measuring reconstruction accuracy, code quality, and query effort.Source: §5 · p. 14

Constrained and formally verified generation

• The paper focuses on which structural information the implementation target should contain, who authors it, and how much uncertainty it removes, unlike prior systems focused on generating code for supplied formal specifications.Its experiments use executable acceptance checks rather than machine-checked proofs; formal checks remain future work.Source: §5 · p. 14

Greenfield and repository-level evaluation

• Program-level benchmarks span short-description function generation and long-horizon iterative greenfield development; this study also examines brownfield modification.The paper reports pass rate alongside specification type, skeleton coverage, model, query effort, and code quality.Source: §5 · p. 14

A Specification Types

• Ten specification types range from task-only descriptions and behavioral requirements to signatures, local contracts, global invariants, architecture documents, and native skeletons.Behavioral requirements include concrete and generalized EARS entries and executable tests; design documents pair requirements with architecture.Source: A Specification Types · pp. 18–19

A.1 Specification templates

• The templates use one hypothetical library-lending module to illustrate the same state-changing loan and state-preserving availability query across specification formats.Examples include executable tests, typed stubs, local contracts, cross-callable invariants, architecture documents, and source-language skeletons with bodies omitted.Source: §A.1 · pp. 19–22

B SDDBench

• SDDBench derives repository-level tasks from real Python libraries, anonymizes names and descriptions, and evaluates reconstructions without reference code or evaluation tests.Functional correctness is the fraction of project evaluation-suite tests passed; anonymization does not completely rule out training-data contamination.Source: B SDDBench · p. 22

C ProgramBench and SCBench

• The experiments evaluate 20 ProgramBench tasks and reconstruct the final repository state for each main SCBench problem.The ProgramBench task list includes atlas, brotli, dropbear, dupl, fzf, and 15 other tasks.Source: C ProgramBench and SCBench · p. 23

D Experimental Details

• Four models were tested on 20 ProgramBench tasks with reference-executable access and nested subsets of available tests, while evaluation tests remained withheld.The study also compared task-only input with EARS prose, original comments, signatures, local contracts, and global invariants; SCBench and SDDBench experiments withheld reference code and evaluation tests.Source: D Experimental Details · p. 23
• ProgramBench query studies varied reference-query counts and compared Global Invariants skeletons with curated examples or uncapped querying; architecture studies compared five nested document versions with task-only input.Architecture versions added components, state, collaborations, layout, and per-file sketches; task and architecture text both counted toward input size.Source: D Experimental Details · p. 23
• Figure 9 compares Sol and Luna on five repositories per benchmark, using nested 25%, 50%, and 75% callable-complexity-ranked local-contract subsets against task-only input and the full skeleton; greater coverage improves pass rates.Adding per-folder descriptions also improves pass rates. In a separate study, error, model cost, and reference calls were tracked through round 8, while code quality was measured at round 8.Source: D Experimental Details · p. 24, Figure 9 · p. 24

E Proofs and remarks for Sections 2 and 3

• For a fixed skeleton, the proof distinguishes acceptable programs within its class from programs in that class agreeing with every tested input.Exact conditioning on the test set is introduced after these definitions.Source: E Proofs and remarks for Sections 2… · p. 24
• Canonical skeletons are defined by a fixed map from programs to skeletons, partitioning the program space; partial skeletons condition on the union of compatible classes.The argument conditions only on positive-probability events and omits zero-weight terms.Source: E Proofs and remarks for Sections 2… · p. 24
• Figure 10 reports that skeletons improve ProgramBench pass rates even when agents can query the oracle executable.Source: Figure 10 · p. 25

• The minimum tests for posterior correctness 1−δ are 2^d−1 under SA but d under SB.Under either uniform prior, a suite leaving at least two candidates has posterior correctness at most 1/2.Source: §E.1 · p. 25
• With standard-basis tests, SA's within-skeleton success is 1/(2^d−d), while the equal-skeleton prior yields posterior correctness 2/(2^d−d+1).The same tests guarantee success under SB.Source: §E.1 · p. 25
• The same reference-labeled sample supplies Θ(2^-d) bits under SA but one bit under SB.The posteriors are uniform on 2^d−1 and 2^(d−1) survivors, respectively.Source: §E.1 · p. 26
• Expected information gain is h2(2^-d) under SA and 1 under SB, averaging over possible responses.These expected mutual informations differ from the information in the same observed response.Source: §E.1 · p. 26

• Under the specified prior, exact identification needs 2^n end-to-end tests versus 4n local tests; the end-to-end bound also holds in the worst case with adaptive queries.At zero error, testing every input suffices for the end-to-end bound, while four input pairs per transition reveal its truth table.Source: §E.2 · p. 26
• Endpoint tests can hide which stage rejected an input because later transitions preserve a state of zero after a mismatch.A local test observes a component before subsequent transitions can erase its effect.Source: §E.2 · pp. 26–27
• This hardness is not depth-only: affine transitions are identified by n+1 endpoint queries, and the exponential claim concerns exact identification under a specified prior.The passage does not establish the bound for every prior or for prediction at fixed nonzero error.Source: §E.2 · p. 27

E.3 Proof of Theorem 2.4

• A mixed suite's minimum cost equals the local costs for passing component classes plus the end-to-end cost to exclude remaining unacceptable combinations.The proof establishes the upper bound by combining suites and the converse by considering any successful mixed suite.Source: §E.3 · p. 27

E.4 Proof of Proposition 2.3

• If the required posterior correctness exceeds the derived ratio, no finite test suite attains it and Nδ(S)=∞.Source: §E.4 · p. 27

E.5 Proof of Proposition 3.1

• Independent component retries take mean 1/α_i proposals each and yield jointly conditioned components; whole-program rejection takes mean ∏1/α_i proposals.The accepted whole program is distributed as q(·|G).Source: §E.5 · pp. 27–28

• A contract-checking component is accepted with false-accept rate ε_i=β_i+(1−β_i)e_i; accepted components remain independent samples from q_i(·|G_i).Source: §E.6 · p. 28
• An accepted component satisfies its contract with probability α_i/[α_i+(1−α_i)ε_i], reaching certainty if α_i=1 or ε_i=0.Source: §E.6 · p. 28
• Independent accepted components all satisfy their contracts with probability ∏1/(1+x_i), bounded below by 1−∑x_i, where x_i=ε_i(1−α_i)/α_i.Source: §E.6 · p. 28
• For whole-program rejection, correctness is α/[α+(1−α)ε]≤α=∏α_i when α<1 and ε>0; it is certain if α=1 or ε=0.Source: §E.6 · p. 28