cs.AIOct 14, 2026
SaveWhen Correctness Feedback Erases Evidence: Phase-Separated Completeness Auditing in Verus
Organizations: Independent Researcher
Abstract
Correctness feedback suppresses the very evidence that specification-completeness auditing is designed to uncover: programs that satisfy a written contract but violate intended behavior. We demonstrate this objective reversal on 12 Verus/Rust tasks across four model families under matched call budgets. Independent no-feedback discovery more than doubles certified-witness yield relative to IntentShield's corrective-feedback loop (59.0% versus 27.1%). A format-matched iterative control places the larger share of this gap in feedback content, not independent restarts. The advantage holds in every model family and survives parser repair. A separate phase-separated execution matches the aggregate yield without reusing responses; most certified witnesses also fail held-out cases. Preserving these witnesses delivers stronger specification repair: Phase-Revised contracts achieve 81.3% implementation success, versus 62.5% for IS-Revised, with Direct-Revised close behind. Both no-feedback witness sources substantially outperform weakened contracts. The effect does not reproduce in the available Dafny and Lean evaluations, establishing an empirical boundary around the studied Verus/Rust workflow. Completeness auditing and correctness repair have opposing immediate objectives. Preserve and certify the admitted failure before repairing it.
Figures & tables
Figure 1: Correctness feedback enters at different times. IntentShield uses it while searching for a witness. Phase uses the same discovery policy as Direct and introduces repair feedback only after the candidate has been frozen. The harness selects the highest-ranked candidate across all three calls (Section 2.1); “final candidate” means the selected output of discovery, not necessarily call 3. The downstream result is from a separate 16-task study.
Figure 2: Certified-witness rates for each Verus task. Each point summarizes 12 model-run outcomes per policy. The plot compares Direct with IntentShield ; the separate Phase execution is assessed by paired-cell agreement in Section 4.5 . The task is the independent unit.
| Policy | Discovery | Certified | Parse failures |
|---|---|---|---|
| Direct | Independent, no feedback | 85/144 (59.0%) | 15/144 |
| FMI | Iterative, dummy feedback | 71/144 (49.3%) | n/r |
| IntentShield | Iterative, real feedback | 39/144 (27.1%) | 49/144 |
| Model-Judgment | Iterative, self-assessment | 34/144 (23.6%) | n/r |
| Phase | Independent, then freeze | 85/144 (59.0%) | n/r |
| Direct pass@1 | First call only | 38/144 (26.4%) | n/r |
Table 1: Primary discovery matrix and matched iterative control. Every full policy uses three calls and the same best-of-three selection rule. Pass@1 evaluates only the first Direct call. Parse counts are episodes with any parse failure, not necessarily the selected candidate; n/r denotes a rate not reported in this comparison.
| Condition | Direct | IntentShield | Difference (pp) |
|---|---|---|---|
| Raw | 85/144 (59.0%) | 39/144 (27.1%) | +31.9 |
| Parser-repaired | 91/144 (63.2%) | 52/144 (36.1%) | +27.1 |
| Parse-clean only | 76/129 (58.9%) | 32/95 (33.7%) | +25.2 |
Table 2: Syntax robustness. Parser repair is applied before certification. Parse-clean filtering is a separate, post-hoc sensitivity analysis with policy-specific denominators, not a matched or causal adjustment.
| Model family | Direct | IntentShield | Difference (pp) |
|---|---|---|---|
| Claude Sonnet 5 | 25/36 (69.4%) | 12/36 (33.3%) | +36.1 |
| DeepSeek V3.2 | 22/36 (61.1%) | 11/36 (30.6%) | +30.6 |
| Devstral 2 | 20/36 (55.6%) | 9/36 (25.0%) | +30.6 |
| Qwen3-Coder-480B | 18/36 (50.0%) | 7/36 (19.4%) | +30.6 |
Table 3: Per-model primary comparison, 36 outcomes per policy and family. The Direct advantage is present in all four families.
Figure 3: Downstream consequences of incomplete and repaired specifications. Panel A compares weakened-contract verification with restored-contract success in the Original condition. Panel B reports successful implementations across all five conditions (16 tasks, three attempts each). True-Spec uses the intended contract. Bars show observed rates, not confidence intervals.
Appendix figures & tables10 assets
Supplementary material from the paper’s appendix.
Appendix
| Model | Bedrock identifier | Use |
|---|---|---|
| Claude Sonnet 5 | global.anthropic.claude-sonnet-5 | A1, A2, Dafny, Lean |
| DeepSeek V3.2 | deepseek.v3.2 | A1 primary |
| Devstral 2 123B | mistral.devstral-2-123b | A1 primary |
| Qwen3-Coder 480B-A35B | qwen.qwen3-coder-480b-a35b-v1:0 | A1, Dafny, Lean |
| Claude Opus 5 | global.anthropic.claude-opus-5 | cross-family diagnostic |
| GLM-5 | zai.glm-5 | cross-family diagnostic |
Table A1: Model identifiers and campaign roles. The first four models form the primary discovery matrix; downstream settings appear in Appendix D.
| Task | Stratum | Omission | Direct | IntentShield | Model-J. | D-IS |
|---|---|---|---|---|---|---|
| cf124A | Residual | Equality | 9/12 | 3/12 | 4/12 | +50.0 |
| cf492A | Residual | Maximality | 8/12 | 3/12 | 3/12 | +41.7 |
| cf92A | Residual | Equality | 7/12 | 2/12 | 2/12 | +41.7 |
| cf271A | Residual | Minimality | 6/12 | 2/12 | 3/12 | +33.3 |
| cf519C | Residual | Maximality | 5/12 | 2/12 | 2/12 | +25.0 |
| cf4A | Total | Output relation | 11/12 | 7/12 | 8/12 | +33.3 |
Table A2: Task-level discovery counts and omitted properties. Each policy contributes 12 outcomes per task. Primary inference compares Direct and IntentShield ; Model-Judgment is secondary.
| Task | Original | IS-Rev. | Phase-Rev. | Task | Original | IS-Rev. | Phase-Rev. |
|---|---|---|---|---|---|---|---|
| cf124A | 0/3 | 2/3 | 3/3 | cf50A | 3/3 | 3/3 | 3/3 |
| cf492A | 0/3 | 2/3 | 3/3 | cf47A | 1/3 | 2/3 | 2/3 |
| cf92A | 0/3 | 1/3 | 2/3 | cf318A | 0/3 | 2/3 | 3/3 |
| cf271A | 1/3 | 2/3 | 3/3 | cf486A | 0/3 | 1/3 | 2/3 |
| cf519C | 0/3 | 2/3 | 3/3 | cf200A † | 1/3 | 2/3 | 2/3 |
| cf4A | 3/3 | 3/3 | 3/3 | cf228A † | 0/3 | 2/3 | 2/3 |
Table A3: Task-level successful implementation attempts out of three for the Original, IS-Revised, and Phase-Revised conditions. A dagger marks the four additional downstream tasks. Three low-yield IS-Revised tasks use highest-ranked available candidates, which may be uncertified; this fallback is not equivalent to certified-witness repair.
Figure 4: The primary Verus direction does not reproduce in the available Dafny and Lean evaluations. The task matrices differ and should not be compared as measures of absolute difficulty.
Figure 5: Parser repair before certification lowers parse-failure rates in both policies but retains a 27.1-point certified-yield difference. Bars show observed episode rates without confidence intervals. The parse-clean sensitivity in Table 2 is a separate post-hoc analysis.
| Task | Omitted property | Candidate | Official disagreement |
|---|---|---|---|
| cf124A | Functional equality | n | Input 3 1 1 ; expected 2, produced 3. |
| cf492A | Maximality | 0 | Input 1 ; expected 1, produced 0. |
| cf271A | Minimality | 9876 | Input 1987 ; expected 2013, produced 9876. |
| cf4A | Output relation | w >= 6 | Input 4 ; expected YES, produced NO. |
| cf110A | Output relation | true | Input 4 ; expected NO, produced YES. |
Table A4: Examples of programs admitted by a weakened contract but rejected by the restored obligation and an official case.
| Phase certified | Phase not certified | Total | |
|---|---|---|---|
| Direct certified | 74 | 11 | 85 |
| Direct not certified | 11 | 48 | 59 |
| Total | 85 | 59 | 144 |
Table A5: Independent Direct / Phase executions on 144 paired cells. Equal totals arise from fresh generation, not identical successful cells.
| Policy | Visible-certified | Held-out disagreement | Conditional rate |
|---|---|---|---|
| Direct | 85 | 79 | 92.9% |
| IntentShield | 39 | 36 | 92.3% |
| Phase | 85 | 78 | 91.8% |
Table A6: Held-out oracle diagnostic using two withheld cases per task. Rates are conditional on visible certification, not all discovery episodes.
| Stratum | Direct | IntentShield | Difference (pp) |
|---|---|---|---|
| Total omission (7 tasks) | 50/84 (59.5%) | 27/84 (32.1%) | +27.4 |
| Residual contract (5 tasks) | 35/60 (58.3%) | 12/60 (20.0%) | +38.3 |
Table A7: Task-stratum yields. Total omissions admit simple constants; residual contracts retain meaningful output obligations.
| Task set | Direct | IntentShield | Difference (pp) |
|---|---|---|---|
| Primary, 12 tasks | 85/144 (59.0%) | 39/144 (27.1%) | +31.9 |
| Extension, 8 tasks | 49/96 (51.0%) | 21/96 (21.9%) | +29.2 |
| Combined, 20 tasks | 134/240 (55.8%) | 60/240 (25.0%) | +30.8 |
Table A8: Benchmark extension. The eight-task extension and combined results are preliminary; the original 12-task matrix is the primary analysis.
More in this topic
Formal Verification
Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.
See all 345 papers