ProofSpend: A Preregistered, Cost-Metered Corpus of LLM Trajectories for Verified Code Generation

The complete execution record of one preregistered study of budget-constrained verified code generation: 5,209 generation units over 870 vericoding tasks (Dafny, Verus, Lean 4), six hosted models, 2,954 trajectory step records with per-step eligibility sets, sampling propensities and safety-rail firings, and a 25,221-entry append-only ledger of list-rate API cost (USD 495.89 confirmatory run plus USD 31.63 stage-1 rerun). Includes the collection harness, frozen task splits with SHA-256 digests, the preregistration with amendments A1-A10, a field-level data dictionary (SCHEMA.md), and an offline analysis script that regenerates the confirmatory results without API access. Version 1.1 corrects the analysis script (intention-to-treat inclusion of 113 never-retried gpt-5.5 one-shot units; all-in cost for 601 A7-retried units; the grid cheat count), its regenerated outputs, and the data dictionary. Every raw record is unchanged; ERRATA.md lists each change. Version 1.0 (10.5281/zenodo.22074866) is kept for historical reference only.