Auditing Acceptance Signals in Verified Code Generation

AI-generated proofs are evaluated, and sometimes selected for training, according to whether a verifier accepts them. Yet this acceptance depends on the toolchain used and the evaluation code that interprets its output. We examine both dependencies in DafnyBench and a released Verus training corpus. In the Verus corpus, a documented change to mutable-reference postconditions accounts for a substantial class of failures. A compiler-guided rewrite restores acceptance for 410 of 442 affected files, including every file recovered by the documented compatibility attribute. The edits are textually invertible, although this does not establish semantic preservation. In DafnyBench, we find that the verification helper accepts summaries reporting zero errors alongside unfinished obligations. Rechecking reference programs across releases also reveals losses and recoveries that aggregate acceptance rates obscure. Together, these findings show why verifier acceptance must be interpreted within its evaluation environment rather than treated as a permanent property of an artifact. They identify a concrete defect in how verification results are scored and a targeted way to recover programs affected by a toolchain change, with implications for evaluating AI-generated proofs and maintaining verifier-filtered training data.