Aditya Vempaty and colleagues separate three questions about AI-written code: did the proof checker accept it, does the proof reference its specification, and does that specification express the user’s requirement?
Dafny, a language with automated mathematical checks, proves the obligations actually written into a program. A successful check can leave the intended functional behavior unspecified.
- In a reproduced Dafny-to-Python workflow, 1,625 of 1,640 HumanEval samples passed verification (99.1%). Among accepted samples, 94.7% lacked a functional result condition.
- Only 1.9% referenced a named specification condition in their promised result. The paper’s proposed check enforces that reference convention; meaningful conditions written directly inside a method can fail it.
- The authors’ stricter Rust workflow verifies every shipped component and enforces the reference check. Still, 124 of 1,080 fully verified MBPP samples failed hidden tests (11.48%).
- Another Rust task set had 229 failures among 1,545 fully verified samples (14.82%). These percentages are conditional on fully verified output, not all attempts.
- A complementary check executes the promised condition against valid and invalid examples. It probes whether the specification admits incorrect results, rather than merely testing generated code.
Caveat: All main experiments use Claude Opus 4.7. Hidden-test failures can also reflect translation, wrapper or test errors, so they do not uniquely diagnose faulty specifications.
A named reference can also point to a meaningless condition. Treat the proposed rule as one structural check, not proof of adequate requirements. Report proof acceptance, structural checks and behavioral tests separately, with their actual denominators.