When Scores Do Not Steer: Auditing Process Credit in Verifier-Guided Repair

Process credit is meant to help a coding agent keep promising intermediate states. That idea only works if the score can change a decision and if the state it prefers is more likely to verify later. We test both conditions in BranchCredit, a width-2 repair controller for Lean and Dafny. Its commitment rule places scalar credit after native verification, an integrity check, and five diagnostic fields. In 216 Lean decisions with multiple candidates, 53 contain a latent disagreement involving credit, but earlier fields settle every choice. Removing credit therefore changes 0/216 selected branches. We then move credit directly below the two hard gates. This promoted rule changes 54/216 selections and 36/144 episode paths, yet changes 0/144 final verification outcomes on the same recorded candidates. A smaller live replay regenerates descendants after forcing the credit-preferred branch: two of five disagreements improve, one worsens, and two do not change. Matched end-to-end evaluations also fail to establish an advantage. On the harder Lean set, BranchCredit solves 29/48 tasks and a branching-matched credit-free controller solves 27/48 (+4.2 percentage points, source-level p=0.50). Other Lean and Dafny comparisons include small positive, exact-null, and negative differences. First-call predictors that look strong on development sources fall toward chance on held-out sources. The result is a practical design test: a process score needs measurable decision authority and held-out continuation value. Without both, it is either unused or unreliable.