The Price of Proof: A Pilot Study of API Cost and Verifier Acceptance in LLM Generation of Formally Verified Code

Formal verification gives LLM-generated code something rare: machine-checked evidence that the code satisfies a fixed specification. A family of benchmarks now reports how often models earn that evidence. None of them reports the bill. We price it on a 30-task, difficulty-stratified pilot of the vericoding benchmark's three verifier ecosystems (Dafny, Verus, Lean 4), across seven hosted models and three prompting regimes, under list-price token metering with every interval task-clustered. Three findings order the spending. Showing the model the formal specification is the cheapest intervention in the study: prompting from the natural-language description alone almost never produced verifier-accepted Verus or Lean code, and every apparent Lean success under that regime had silently dropped the required theorem, a failure a spec-integrity audit catches and acceptance rates alone do not. Verifier-feedback repair prices as a ladder with a cheap top rung: the first repair round buys more acceptance per dollar than all deeper rounds together. And the posted price list is an unreliable guide to delivered cost: on the six Lean tasks both models completed, the model listed at 1.7x its sibling's per-token rate delivered each accepted function 2.8x cheaper, a gap carried by acceptance, all six accepted against two. Separately, hidden reasoning tokens dominate billed output where providers expose them, so the meter, not the menu, sets the bill. We propose cost per verifier-accepted function, reasoning tokens included, as the quantity benchmarks should report beside acceptance: it prices a repair round against the acceptance it buys, and it ranks models in the order their delivered dollars fall rather than the order the price list assigns.