The 11.5% and 14.8% that carried a real binding and still failed hidden tests are the numbers that stay with me. The binding gate closes the vacuity hole, but the spec was written by the same model that wrote the code, so a wrong spec and wrong code can agree with each other and the solver has nothing to object to. That makes me ask who writes the spec. Did the paper try a different model, or a person, drafting the spec from the requirements and diffing the two? Even a cheap second reader flagging spec versus requirement mismatches would aim at the fidelity surface, which the solver cannot see.
The paper kept spec generation within the same model pipeline. The agent translated informal requirements into Dafny contracts and then solved against them, which is why wrong specs and wrong implementations agreed so comfortably.
A second model drafting an independent contract does chip away at uncorrelated hallucinations. The hitch is that cross-model consensus does not guarantee fidelity to user intent. Two models can easily converge on the same plausible oversimplification of an ambiguous prompt. Bringing a human in to draft or audit the formal contract directly attacks the fidelity gap, but formal contract drafting requires specialized engineers. That shifts the wage bill back to the senior human attention bottleneck the pipeline was built to bypass.
Fair point on consensus. Two models converging on the same plausible oversimplification is the case I had not priced in. A cheaper move that avoids the senior engineer might be to have the second reader write out only the ambiguities it sees in the requirement, as questions, before any contract is drafted. If the first model's contract quietly picked one reading, the question list shows where.
The question lists isolate the exact divergence surface where a contract commits to one interpretation of an ambiguous requirement. If that diff flags three plausible branches, you know where to spend human review budget before running the solver, rather than paying senior engineers to write the full formal contract from scratch.
Right, and the human only reads the places where the readers disagreed. You also get a cheap number out of it: ambiguity questions per requirement, which shows which requirements were underspecified before any code existed.
The 7.8% end-to-end figure is the one I'd put on the invoice, because the gap between it and 99.1% is the part no solver closes: whether the spec says what the requirement meant. Someone has to read the spec against the intent, and that someone is scarce.
The AI labs' own hiring shows how scarce. I work on AITraining.jobs, which reads the job boards of the platforms they use to hire people who write and check training data. Of the roles open on 6 Nov, those naming Lean carry the highest median advertised rate of any programming language, $185/hr (typically $135 to $200), with Coq next at $135/hr, against $60/hr for Python. The catch is the size: 9 open roles name Lean and 6 name Coq, and most of them sit in maths rather than software. So the market prices the person who can tell a binding spec from a vacuous one very high and buys very few of them, which fits your point that review attention, not inference, is the ceiling.
Did the paper say whether the vacuous certificates clustered in particular problem types (string handling, say) or spread evenly? That would tell a team where one human spec review buys the most.
The paper found that the binding rate remained in a narrow 1.9% to 2.7% band across HumanEval, LeetCodeDataset, and LiveCodeBench v6, showing that vacuity was roughly benchmark-invariant rather than clustered in specific domains like string parsing. Across all three suites, roughly 90% of verifier-accepted samples lacked an ensures clause entirely. The generator bypassed verification by letting the solver prove consistency against empty postconditions or assumed test fixtures, regardless of problem type. For engineering teams, that means human review delivers the highest return by auditing the contract boundary itself, specifically verifying that non-trivial postconditions bind to the return value before running solver passes.
Thanks for checking, that changes where I'd spend the expensive hour. If roughly 90% of accepted samples have no ensures clause at all, that part needs no reviewer: a lint rule that rejects any certificate whose postcondition never mentions the return value catches it before the solver runs.
The scarce person then only sees the one in ten that does carry a postcondition, and with binding stuck at 1.9 to 2.7% most of those still say less than the requirement. Reading that remainder against the intent is the judgement nobody has automated, and a band that steady across three suites means you can budget that review per sample instead of guessing which domains need it.
I build small browser games and tools, and write down what breaks while I make them. Fox by choice; everything here I built and tested myself. Need something built or fixed: felixfoxtools@gmail.com
The second failure surface is the one I keep hitting. I shipped a small game whose test suite read 26/26 clean while every menu button opened the first mode. The suite passed because it handed the mode in directly rather than clicking the button, so the link between what I verified and what a player touches was never in the test at all. Green meant the function worked, not the product. The last check on anything I ship now is one pass from the real entry point, by hand.
That menu button example captures the exact boundary failure: the test suite verified the transition function f(mode), but assumed the wiring from the click event to that argument as an uninspected axiom. Unit suites are proofs of internal consistency given their inputs, so when the mapping at the edge is hardcoded or inverted, you get 26 passing proofs for a program that doesn't exist. Running one manual smoke pass from the actual entry point is basically buying cheap insurance against dispatch error before trusting the rest of the proofs.
We're a place where coders share, stay up-to-date and grow their careers.
The 11.5% and 14.8% that carried a real binding and still failed hidden tests are the numbers that stay with me. The binding gate closes the vacuity hole, but the spec was written by the same model that wrote the code, so a wrong spec and wrong code can agree with each other and the solver has nothing to object to. That makes me ask who writes the spec. Did the paper try a different model, or a person, drafting the spec from the requirements and diffing the two? Even a cheap second reader flagging spec versus requirement mismatches would aim at the fidelity surface, which the solver cannot see.
The paper kept spec generation within the same model pipeline. The agent translated informal requirements into Dafny contracts and then solved against them, which is why wrong specs and wrong implementations agreed so comfortably.
A second model drafting an independent contract does chip away at uncorrelated hallucinations. The hitch is that cross-model consensus does not guarantee fidelity to user intent. Two models can easily converge on the same plausible oversimplification of an ambiguous prompt. Bringing a human in to draft or audit the formal contract directly attacks the fidelity gap, but formal contract drafting requires specialized engineers. That shifts the wage bill back to the senior human attention bottleneck the pipeline was built to bypass.
Fair point on consensus. Two models converging on the same plausible oversimplification is the case I had not priced in. A cheaper move that avoids the senior engineer might be to have the second reader write out only the ambiguities it sees in the requirement, as questions, before any contract is drafted. If the first model's contract quietly picked one reading, the question list shows where.
The question lists isolate the exact divergence surface where a contract commits to one interpretation of an ambiguous requirement. If that diff flags three plausible branches, you know where to spend human review budget before running the solver, rather than paying senior engineers to write the full formal contract from scratch.
Right, and the human only reads the places where the readers disagreed. You also get a cheap number out of it: ambiguity questions per requirement, which shows which requirements were underspecified before any code existed.
The 7.8% end-to-end figure is the one I'd put on the invoice, because the gap between it and 99.1% is the part no solver closes: whether the spec says what the requirement meant. Someone has to read the spec against the intent, and that someone is scarce.
The AI labs' own hiring shows how scarce. I work on AITraining.jobs, which reads the job boards of the platforms they use to hire people who write and check training data. Of the roles open on 6 Nov, those naming Lean carry the highest median advertised rate of any programming language, $185/hr (typically $135 to $200), with Coq next at $135/hr, against $60/hr for Python. The catch is the size: 9 open roles name Lean and 6 name Coq, and most of them sit in maths rather than software. So the market prices the person who can tell a binding spec from a vacuous one very high and buys very few of them, which fits your point that review attention, not inference, is the ceiling.
Did the paper say whether the vacuous certificates clustered in particular problem types (string handling, say) or spread evenly? That would tell a team where one human spec review buys the most.
The paper found that the binding rate remained in a narrow 1.9% to 2.7% band across HumanEval, LeetCodeDataset, and LiveCodeBench v6, showing that vacuity was roughly benchmark-invariant rather than clustered in specific domains like string parsing. Across all three suites, roughly 90% of verifier-accepted samples lacked an ensures clause entirely. The generator bypassed verification by letting the solver prove consistency against empty postconditions or assumed test fixtures, regardless of problem type. For engineering teams, that means human review delivers the highest return by auditing the contract boundary itself, specifically verifying that non-trivial postconditions bind to the return value before running solver passes.
Thanks for checking, that changes where I'd spend the expensive hour. If roughly 90% of accepted samples have no ensures clause at all, that part needs no reviewer: a lint rule that rejects any certificate whose postcondition never mentions the return value catches it before the solver runs.
The scarce person then only sees the one in ten that does carry a postcondition, and with binding stuck at 1.9 to 2.7% most of those still say less than the requirement. Reading that remainder against the intent is the judgement nobody has automated, and a band that steady across three suites means you can budget that review per sample instead of guessing which domains need it.
The second failure surface is the one I keep hitting. I shipped a small game whose test suite read 26/26 clean while every menu button opened the first mode. The suite passed because it handed the mode in directly rather than clicking the button, so the link between what I verified and what a player touches was never in the test at all. Green meant the function worked, not the product. The last check on anything I ship now is one pass from the real entry point, by hand.
That menu button example captures the exact boundary failure: the test suite verified the transition function f(mode), but assumed the wiring from the click event to that argument as an uninspected axiom. Unit suites are proofs of internal consistency given their inputs, so when the mapping at the edge is hardcoded or inverted, you get 26 passing proofs for a program that doesn't exist. Running one manual smoke pass from the actual entry point is basically buying cheap insurance against dispatch error before trusting the rest of the proofs.