The Missing Proof in the Prompt
AI programming agents are often described as if their main problem were insufficient instruction. Give the model a longer system prompt, add more examples, specify more rules, and perhaps it will behave like a careful engineer. This series examines a different problem: coding agents can produce text that looks like software without possessing reliable evidence that the software works. The practical judgment for the reader is how to distinguish an instruction, an agent action, and an observation that the resulting program actually behaves as intended.
That distinction matters because the subject is no longer a model completing an isolated line of code. A programming agent can inspect a repository, edit several files, invoke tools, run tests, react to errors, and decide when to stop. Its work unfolds in an environment. The quality of the final patch depends not only on what the agent can say about code, but on what happens when the code is compiled, executed, measured, and placed back into a living system.
When plausible code meets the real program
A language model trained mainly on static code learns many things that are visible in text: syntax, common API patterns, signatures, documentation conventions, and the shape of familiar solutions. What it receives much less often is the behavior that appears only after execution: a crash, a wrong output, a timing measurement, a memory trace, a coverage map, or a diagnostic from a sanitizer. The difference is not cosmetic. It separates recognizing a plausible implementation from knowing what that implementation does.
The consequences show up in several forms. An agent may call an interface with the wrong shape or type. It may generate a function that appears coherent but fails on its first input. It may preserve the answer while claiming to have improved performance, even though the program runs no faster. Or it may infer that a fix is correct because the surrounding text sounds persuasive. These are different symptoms of the same missing signal: the agent has been asked to reason about behavior without being given enough evidence of behavior.
This is why ordinary prompt escalation has a ceiling. A prompt can describe the desired result, point to relevant files, state constraints, propose a plan, or tell an agent to run tests. It can improve what the agent attends to. It cannot, by its wording alone, reveal whether a candidate actually passes an unseen edge case, preserves a repository interface, reduces runtime, or breaks an assumption hidden inside a dependency. Those facts belong to the program’s execution, not to the eloquence of the request.
The distinction is especially important in repository work. A short code-completion task can sometimes be judged with a handful of input-output examples. Real software often depends on configuration, files, custom objects, imported helpers, environment state, and conventions that are not contained in one function. The agent must understand an interface it did not invent and change code without disturbing behavior elsewhere. A text-only evaluator can reward a convincing imitation while missing the failure that a developer would encounter as soon as they run the project.
The repository experiments in the dissertation make that difficulty visible without requiring a dramatic failure story. Their synthesized tasks combine a function with its surrounding repository context and an equivalence harness that runs the original implementation as a reference. On those tasks, the strongest reported model reached only about half-pass performance, and performance fell as targets required more dependencies or multiple files. The reported comparison also found that chain-of-thought-style planning did not improve the cited static result. By contrast, when the agent received concrete interpreter feedback, repeated repair recovered a substantial share of its initial failures. The lesson is not that an agent should stop planning. It is that planning describes a proposed path, while execution reveals whether the path has reached the intended state.
The Berkeley dissertation that organizes this series calls this the static-code-versus-runtime-behavior gap. Its claim is not that language models know nothing about execution, nor that every failure has one cause. It is that static corpora alone do not provide the behavioral supervision needed to make runtime properties directly measurable. That framing turns a vague complaint—“the agent is unreliable”—into an engineering question: what artifact will expose the property we care about?
A prompt states intent; evidence has to be produced
The answer is an executable specification: a runnable artifact that takes a candidate program and produces a usable signal by executing the program or observing its traces. The signal might be a pass/fail verdict, a speedup ratio, or a runtime invariant. The important word is runnable. The specification does not merely tell the agent what good behavior would sound like. It creates a procedure through which behavior can be observed.
This makes an executable specification an intermediate form. Natural-language requirements are expressive and necessary, but they can be ambiguous and are not automatically verifiable. Formal contracts can be precise, but writing and checking them may require substantial expertise and infrastructure. A runnable test, input generator, equivalence harness, performance workload, or dynamic observation occupies a more practical middle ground. It provides evidence about selected behaviors without claiming to prove every behavior for every possible input.
That last qualification is essential. A test suite is not reality; it is a measurement instrument. It sees the inputs it exercises and the properties it checks. A performance harness can establish that a patch reaches a target on a workload while saying nothing about maintainability or memory use. A generated test can expose a bug, but it can also be invalid, redundant, or too weak to distinguish a correct patch from an incorrect one. The value of execution-backed feedback therefore depends on how well the artifact represents the intended behavior and how carefully its blind spots are understood.
The form of the artifact should follow the failure we are trying to prevent. If the question is functional correctness, a test can exercise inputs and compare outputs. If the question is whether a repository change preserves an existing implementation, an equivalence harness can run both versions on the same cases. If the question is performance, correctness must be paired with a workload and a measurement rather than inferred from a smaller-looking patch. If the source text hides runtime structure—such as aliasing or allocation size—an observation of executions may be more informative than another prose description. These are not interchangeable tools. Each makes one property visible and leaves others outside its field of view.
The difference from a longer prompt is visible in the feedback loop:
The prompt remains important at the beginning of this loop. It supplies intent, context, priorities, and constraints that a test runner cannot invent. But the prompt is not the final authority over whether the candidate works. Execution supplies a different kind of information, and the agent can use that information to repair a failure, select among alternatives, or stop before presenting an unverified result.
The evidence in the dissertation makes this distinction concrete. In its repository-level experiments, chain-of-thought-style planning did not improve the cited static code-generation result. When an interpreter and an equivalence harness supplied concrete error feedback, however, the agent recovered a meaningful portion of its initially failing attempts through iterative repair. That does not show that planning is useless. It shows that an explanation of what the agent intends to do is not the same as an observation of what the program did.
One idea, several jobs—and a larger definition of reliability
Executable specifications become more powerful when they are treated as a shared feedback mechanism rather than as a final exam. The dissertation groups their uses into three roles.
First, they measure. A benchmark can run a candidate against generated inputs, a reference implementation, hidden tests, or a timed workload. The resulting score is tied to a behavior that the evaluator deliberately chose to observe. Second, they supply training signal. The same tests can filter trajectories, label examples, define an environment, or become a reward. Third, they guide inference. An agent can run checks while repairing a patch, or use tests and learned judgments to choose one candidate from many sampled trajectories.
A later case extends the idea further: when a task is too long for one final test to guide safely, runtime observations can be attached to intermediate steps. Per-function equivalence checks and dynamic properties can help a translation system decide what a C pointer means before it commits to a safe Rust representation. The specification then does more than judge the finished artifact. It makes the path through a difficult task observable one decision at a time.
Yet reliable coding agents are not defined by functional correctness alone. A human-centered study of enterprise coding-agent rules found expectations around following standards and project workflows, producing readable and maintainable code, understanding context before acting, validating work proactively, working incrementally, communicating clearly, asking for help, analyzing trade-offs, and learning from feedback. These requirements are often expressed in prompts or persistent rules because they concern how an agent works with a team, not only whether a function returns the expected value.
The combination is more demanding than a checklist of good manners. Users want bounded agency: the agent should follow local standards and stay within the requested scope, but it should also notice uncertainty, ask for clarification, and explain a trade-off before an irreversible choice. They want autonomy inside a workflow that remains legible to the people responsible for the code. That is why “run the tests” is only one part of a reliable process. The agent may also need to show that it understood the project context, changed the right abstraction, preserved maintainability, and stopped at a point where a human can still review the decision.
The same study argues that expectations shift with the work. Production engineering puts more weight on reliability, conventions, and long-term code health; rapid prototyping may put more weight on exploration, explanation, and visual or interaction quality. A fixed prompt can state a preference, but an evaluation system must know which preference matters in the current setting. The question is therefore not only whether a check runs, but whether it observes the behavior that this task and this relationship actually require.
That creates the series’ second qualification. The answer is not to replace every prompt with a test, because some requirements are contextual, social, or value-laden. Nor is it enough to leave every requirement as prose, because a statement such as “validate your work” is weaker than a system that can actually run the relevant checks and show the result. A trustworthy agent needs both: language for intent and collaboration, plus executable or reviewable evidence for properties that must hold in the world.
The central question, then, is not whether an agent has been given enough words. It is whether the system has supplied the right evidence at the right point in the agent’s work. The chapters that follow examine that question from several angles: how executable contracts change evaluation, how they become training environments and rewards, how they select among candidate solutions, how local checks support long-horizon work, and how technical verification must be joined to human-centered judgment. The goal is not a universal score for reliability. It is a way to see what an agent has actually demonstrated—and what it has merely described.