当正确性反馈抹去证据：Verus 中的分阶段完备性审计

# Phase-Separated Completeness Auditing in Verus
Source: [https://arxiv.org/html/2610.20676](https://arxiv.org/html/2610.20676)
## When Correctness Feedback Erases Evidence: Phase\-Separated Completeness Auditing in Verus

###### 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 toIntentShield’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\.

Accepted at the NeurIPS 2026 Workshop on AI for Verifiable Coding\.

Keywords:formal verification; specification completeness; Verus; large language models; adversarial testing; program synthesis; correctness feedback

## 1\. Introduction

Verification success does not establish specification completeness\. A verifier can discharge every written obligation while the resulting program still violates its author’s intent\. The proof is valid; the contract is missing a requirement\.

A completeness audit must therefore find a program that the contract accepts but the task rejects\. We call it a*specification\-completeness witness*\. The wrong program is not an unsuccessful implementation to discard: it is concrete evidence of what the contract forgot to forbid\.

Correctness feedback changes roles under this objective\. In ordinary synthesis, a failed proof or test tells the model what to repair\. During completeness auditing, correcting an admitted wrong program removes the evidence the audit needs\. We call this conflict the*objective reversal*\. Our experiments show that a conventional feedback loop incurs a large discovery penalty in Verus, even though the prompt continues to request a counterexample\.

Our primary comparison covers three policies\.Directmakes independent adversarial attempts without corrective feedback\.IntentShieldfeeds compilation, verifier, and visible\-test results back into discovery\.Phaseis a separate execution of the same discovery protocol asDirect, followed by a frozen handoff to certification and repair\. To separate feedback content from iterative conditioning, we also evaluate a Format\-Matched Iterative control \(FMI\), which retains candidate history and theIntentShieldprompt template but replaces semantic feedback with fixed, unevaluated feedback fields\. Model\-Judgment adds model self\-assessment and is a secondary policy\. Downstream, we compare three repaired\-specification conditions with the weakened and fully specified intended contracts\.

The primary comparison tests two practical deployment strategies: fresh independent sampling and feedback\-loop refinement\. The matched iterative control then separates the feedback\-content contrast from the independent\-restart contrast while retaining prompt structure and candidate history\. The no\-feedback advantage holds across all four model families, survives parser repair, and carries into downstream contract repair\. It does not reproduce in the available Dafny or Lean evaluations: the established result is specific to the studied Verus/Rust workflow\.

We make three contributions:

- •We demonstrate that corrective feedback suppresses certified witnesses in Verus, with matched iterative controls and per\-model evidence separating feedback\-content and independent\-restart contrasts;
- •We establish a preserve\-before\-repair workflow whose separate execution retains aggregate discovery yield, with cell\-level correspondence and held\-out counterexamples; and
- •We show that preserved witnesses produce stronger specification repairs, with Direct\-Revised and True\-Spec controls and explicit cross\-substrate tests\.

### 2\.1\. Certified witnesses

LetS−S^\{\-\}be a contract with one meaningful postcondition removed\. A candidate programppis a certified completeness witness when:

1. 1\.ppverifies underS−S^\{\-\};
2. 2\.restoring the omitted postcondition makes verification fail;
3. 3\.ppcompiles and executes; and
4. 4\.ppdisagrees with at least one official test case\.

Each episode produces three candidates\. The harness ranks them lexicographically by parse success, weakened\-contract acceptance, Rust compilation, visible\-test divergence count, and then earliest call index\. Only the selected candidate is certified, regardless of call index: the final call is not automatically chosen\. In 11 of the 39 certifiedIntentShieldepisodes, call 1 or call 2 outranks call 3\. Selection uses 16 visible oracle cases; certification replays the selected candidate against the restored contract and complete official oracle bank\. Because visible cases can satisfy the behavioral\-disagreement criterion, the primary evaluation demonstrates specification incompleteness, not held\-out generalization\. A separate check with two withheld oracle cases per task is reported in Section[4\.7](https://arxiv.org/html/2610.20676#S4.SS7)\. Eight mutation examples per task guide search but do not independently certify wrongness\.

These gates separate whether the weaker contract admits the candidate, whether the omitted obligation changes verification, and whether executable behavior is wrong on an intended input\. Failure to verify the restored contract is not itself proof of a behavioral counterexample; the official\-case disagreement supplies that separate evidence\. Passing the weaker contract does not make a candidate a witness if it computes the intended answer\.

### 2\.2\. Separating discovery from repair

Figure[1](https://arxiv.org/html/2610.20676#S2.F1)shows the central distinction\.IntentShieldkeeps corrective feedback inside the discovery loop, allowing later calls to revise earlier candidates\.Phasefirst searches without that feedback, freezes the exact candidate, and only then certifies the witness and repairs the specification\.

![Refer to caption](https://arxiv.org/html/2610.20676v1/publication/plots/intent_shield_workflow.png)Figure 1:Correctness feedback enters at different times\.IntentShielduses it while searching for a witness\.Phaseuses the same discovery policy asDirectand 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\.Phase separation enforces an explicit boundary between discovering an admitted failure and correcting it\. Its contribution is the auditable handoff, not a different search algorithm\. Discovery used prompts and settings byte\-identical toDirect, but separate API requests issued 48 hours later, with fresh request identifiers and timestamps and no reused responses\. The separate execution retains the full aggregate discovery yield before passing certified evidence to repair\. The matching 85/144 totals include cell\-level variation, quantified in Section[4\.5](https://arxiv.org/html/2610.20676#S4.SS5)\.

## 3\. Experimental design

### 3\.1\. Verus tasks

We use 12 functions from VeriContest\[[1](https://arxiv.org/html/2610.20676#bib.bib1)\]with Verus\[[3](https://arxiv.org/html/2610.20676#bib.bib3)\]\. For five*residual\-contract*tasks, removing one postcondition leaves another meaningful output constraint\. For seven*total\-omission*controls, the complete output relation is removed while input preconditions remain\. Appendix[C](https://arxiv.org/html/2610.20676#A3)lists every task and omission\.

Candidates are side\-effect\-free Rust expressions\. Every selected candidate is checked under the weakened and restored contracts, compiled as Rust, and evaluated on official cases\.

All 12 tasks, omission types, and the eight hand\-written mutation examples per task were fixed before the first model query\. Eligible tasks have at least three official oracle cases and a removable postcondition yielding a syntactically valid, weaker contract\. Omission types were determined by specification structure, not model outputs\. Weakening removes the output relation for total\-omission controls or relaxes an equality/extremality clause for residual\-contract tasks\. No task was added, removed, or re\-weakened in response to model behavior\. The four additional downstream tasks,cf200A,cf228A,cf263A, andcf337A, were selected before A2 using the same weakening protocol and are excluded from the primary matrix\.

### 3\.2\. Discovery policies

#### Direct\.

Three independent calls request a program that satisfies the weakened contract but violates the task\. No candidate, verifier result, or visible\-test result is carried between calls\.

#### IntentShield\.

Each new call receives the previous candidate together with compilation, weakened\-contract, and visible\-test feedback\. The prompt continues to request an admitted wrong program, but the interaction resembles a conventional repair loop\.

#### Model\-Judgment\.

Each new call receives the previous candidate and asks the model to assess whether it verifies under the weakened contract, violates intended behavior, and constitutes a valid witness before revising it\. This feedback policy is part of the complete campaign but not the primary inferential comparison\.

#### FMI\.

One fresh call and two revisions preserve theIntentShieldprompt template and previous\-candidate context\. The feedback block is replaced by “compilation: \[not evaluated\], verification: \[not evaluated\], tests: \[not evaluated\]”\. Prompt length is matched to within 3%\. The template retains the same output\-format instructions, including the absence of “ONLY” in calls 2 and 3\. ThusFMIis also the sequential, previous\-candidate\-conditioned no\-feedback arm\.

#### Phase\.

Discovery is identical toDirect\. The chosen candidate is then frozen and certified before any specification repair or correctness\-oriented implementation work begins\.

### 3\.3\. Primary matrix

The primary matrix covers 12 tasks, four model families, three labeled repeat episodes, and four executed policies, giving 144 outcomes per policy and 1,728 model calls in the original four\-policy campaign\. The matchedFMIcontrol adds 144 outcomes under the same task/model/repeat design and three\-call budget\. Primary inference comparesDirectandIntentShield; Model\-Judgment is secondary\. The model families are Claude Sonnet 5, DeepSeek V3\.2, Devstral 2, and Qwen3\-Coder\-480B\. Each\(task,model,method\)\(\\text\{task\},\\text\{model\},\\text\{method\}\)combination has three repeat episodes, identified by tracking labels 17, 43, and 101; each episode contains three calls\. The labels are not provider seeds\. The task is the independent unit, and within\-task episodes are repeated stochastic samples rather than independent observations\.

The primary campaign ran in September 2026 through Amazon Bedrock inus\-west\-2\. Appendix[A](https://arxiv.org/html/2610.20676#A1)gives the exact Runtime, inference\-profile, and Mantle identifiers\. Within each model, policies received matched three\-call budgets\. Optional sampling controls were omitted, so provider defaults applied\. Claude Sonnet 5 used its default adaptive\-thinking configuration and default high effort\. Runtime open\-weight routes used their provider\-default decoding parameters\. Transient transport failures were retried with the campaign’s adaptive retry policy, while parse failures remained in the denominator\. The matched control uses the same endpoints and decoding defaults\. Prompt templates with formatting normalized for print appear in Appendix[B](https://arxiv.org/html/2610.20676#A2)\.

### 3\.4\. Downstream evaluation

Campaign A2 uses the 12 primary tasks and four additional VeriContest tasks\. Each specification condition receives three implementation attempts per task:

- •Original:the weakened specification;
- •IS\-Revised:repair using the highest\-rankedIntentShieldcandidate;
- •Direct\-Revised:repair using a certifiedDirectwitness;
- •Phase\-Revised:repair using a certified, phase\-preserved witness; and
- •True\-Spec:the fully specified intended contract, an oracle reference\.

All three implementation attempts use Claude Sonnet 5 and are independent fresh calls with the same specification; no candidate or feedback carries over between attempts\. All attempts enter the denominator, giving 48 per condition\. For three low\-yield tasks whereIntentShieldcertifies zero or one witnesses, IS\-Revised uses its highest\-ranked available candidate, which need not be fully certified\.Phasehas at least one certified witness for every downstream task\. The four additional tasks receive the sameDirect,Phase, andIntentShielddiscovery cycle with four models and three episodes per model\. Thus IS\-Revised measures the complete selection\-and\-repair workflow, including fallbacks, rather than repair conditional on certification\. Appendix[D](https://arxiv.org/html/2610.20676#A4)gives downstream settings and task\-level results; Appendix[B](https://arxiv.org/html/2610.20676#A2)gives the repair and synthesis templates\.

### 3\.5\. Analysis

For the primary result, each task contributes itsDirect\-minus\-IntentShielddifference over 12 model\-run outcomes\. We report the mean task effect, a task\-cluster bootstrap interval, and an exact two\-sided sign test\. Downstream comparisons use the difference in successful attempts within each task; ties are omitted from the sign test\. We explicitly label one\-sided exploratory sign tests\. TheFMIgap decomposition is a difference of observed rates, not a formal mediation analysis\. Cell correspondence, held\-out\-case checks, and failure categories are descriptive diagnostics\.

## 4\. Results

### 4\.1\. Corrective feedback suppresses witnesses

Figure 2:Certified\-witness rates for each Verus task\. Each point summarizes 12 model\-run outcomes per policy\. The plot comparesDirectwithIntentShield; the separatePhaseexecution is assessed by paired\-cell agreement in Section[4\.5](https://arxiv.org/html/2610.20676#S4.SS5)\. The task is the independent unit\.Directcertifies 85 of 144 outcomes \(59\.0%\), compared with 39 of 144 \(27\.1%\) forIntentShield: corrective\-feedback discovery produces fewer than half as many certified witnesses under the same call budget\. The mean task\-level difference is 31\.9 percentage points, with a task\-bootstrap 95% interval of \[21\.5, 38\.9\]\. Eleven tasks favorDirectand one favorsIntentShield, giving an exact two\-sided sign\-testp=0\.00635p=0\.00635\.

The suppression extends to both task strata\. The difference is 38\.3 points on the five residual\-contract tasks and 27\.4 points on the seven total\-omission controls\. The only reversal iscf50A, whereIntentShieldcertifies four outcomes andDirectcertifies two\. The larger residual\-contract gap rules out a result confined to tasks with the entire output relation removed\.

### 4\.2\. Feedback content dominates the observed gap

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 firstDirectcall\. Parse counts are episodes with any parse failure, not necessarily the selected candidate; n/r denotes a rate not reported in this comparison\.FMIcertifies 71/144 outcomes \(49\.3%; Table[1](https://arxiv.org/html/2610.20676#S4.T1)\)\. The 31\.9\-pointDirect–IntentShieldgap decomposes into 22\.2 points forFMIminusIntentShield\(69\.6% of the gap\) and 9\.7 points forDirectminusFMI\(30\.4%\)\. The matched comparison rejects a protocol\-only explanation: removing semantic feedback within the same iterative structure recovers 32 certified witnesses\. Candidate conditioning and lost restart diversity matter, but their rate contrast is less than half the feedback\-content contrast\. Model\-Judgment is not an anchoring\-only control: its assessment step changes the semantic instructions, so its 34/144 yield cannot isolate anchoring from self\-evaluation\.

Directpass@1 certifies 38/144 \(26\.4%\), close to the fullIntentShieldloop’s 39/144 \(27\.1%\)\. Thus the primary advantage is not present in a single fresh draw; it emerges under the three\-call deployment budget\. For illustration, three independent draws with a common success probability38/14438/144would give1−\(1−38/144\)3=60\.1%1\-\(1\-38/144\)^\{3\}=60\.1\\%at least\-one success, close to the observed 59\.0%\. This is not a fitted independence model: task and model success probabilities are heterogeneous, and the harness selects one candidate rather than certifying every draw\.

The policy ordering is clear: independent discovery \(59\.0%\), iterative dummy feedback \(49\.3%\), iterative external feedback \(27\.1%\), and iterative self\-assessment \(23\.6%\)\. Iteration without semantic feedback preserves far more witnesses than either feedback\-bearing loop\. These comparisons establish a policy\-level discovery penalty, not an internal model mechanism\. Restoring “ONLY” inIntentShieldcalls 2 and 3 yields 41/144 witnesses \(28\.5%\), only 1\.4 points above the original loop: that output\-instruction change does not recover the lost yield\.

### 4\.3\. The discovery gap survives parser repair

We apply a parser\-repair wrapper to each candidate before certification\. The wrapper closes unmatched brackets, removes semicolons, and extracts the expression from surrounding text\. It does not use verifier or test outcomes to choose a behavioral rewrite\. The same wrapper is applied to both policies; the compilation, weakened\-contract, restored\-contract, and behavioral gates are then rerun on the resulting expression\.

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\.Parse\-failure rates fall from 34\.0% to 11\.8% forIntentShieldand from 10\.4% to 4\.2% forDirect\.IntentShieldgains 13 certified outcomes whileDirectgains six\. The between\-policy count difference falls from 46 to 39, retaining 84\.8% of the original gap\. Repairing syntax recovers witnesses but leaves the central discovery penalty intact\. The intervention is partial: residual parse failures remain and constrained decoding is not evaluated\. Nevertheless, raw, parser\-repaired, and parse\-clean analyses all retain a difference exceeding 25 points\.

### 4\.4\. Every model family favors no\-feedback discovery

Table 3:Per\-model primary comparison, 36 outcomes per policy and family\. TheDirectadvantage is present in all four families\.Every family exhibits a large no\-feedback advantage: the gaps range from 30\.6 to 36\.1 points \(Table[3](https://arxiv.org/html/2610.20676#S4.T3)\)\. All four favorDirect\(descriptive one\-sided sign test,p=0\.0625p=0\.0625\)\. The primary inference remains task\-level\.Directleads on 10 of 12 tasks within Claude, 10 within DeepSeek, nine within Devstral, and 10 within Qwen\. Claude has the highest absolute rates for both policies, but no family reverses the aggregate direction\.

### 4\.5\. Phase separation preserves discovery

Phasealso certifies 85/144 outcomes, but not in exactly the same cells\. Of 144 task/model/repeat cells, 74 certify in both runs, 48 in neither, and 11 in each direction are discordant \(Appendix[G](https://arxiv.org/html/2610.20676#A7)\)\. Agreement is 122/144 \(84\.7%; Cohen’sκ=0\.68\\kappa=0\.68\)\. Only 31/74 co\-certified witnesses \(41\.9%\) are string\-identical; the other 43 are distinct expressions that independently pass all four certification gates\. Fresh request identifiers and timestamps distinguish the executions, separated by 48 hours; no responses were reused\. Equal aggregate yield therefore comes from fresh generation rather than output reuse\. The separate Verus execution preserves aggregate discovery strength under the shared harness and selection rule\. Task totals match for 10 of 12 tasks;cf47Aandcf486Aeach differ by one outcome in opposite directions\. An independent\-draw calculation using empirical cell success probabilities gives 83\.1% expected agreement, near the observed 84\.7%\. This is a descriptive consistency check, not proof of independence across cells or semantic equivalence between distinct expressions\.

### 4\.6\. Preserved witnesses deliver stronger downstream repair

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\.In the Original condition, 42 of 48 implementations verify against the weakened contract, but only 14 verify after the missing postcondition is restored\. This 58\.3\-point gap exposes the practical cost of an incomplete contract: high verification yield can coexist with low success against the intended specification\.

Phase\-Revised specifications produce 39/48 successful implementations \(81\.3%\), Direct\-Revised 37/48 \(77\.1%\), IS\-Revised 30/48 \(62\.5%\), Original 14/48 \(29\.2%\), and True\-Spec 44/48 \(91\.7%\)\. Phase\-Revised exceeds IS\-Revised on nine tasks and ties on seven, with no losses \(p=0\.003906p=0\.003906, two\-sided sign test\); the mean difference is 18\.8 points \(\[10\.4, 27\.1\]\)\. Phase\-Revised also exceeds Original on 13 tasks and ties on three \(p=0\.000244p=0\.000244, two\-sided sign test\)\. Direct\-Revised exceeds IS\-Revised by 14\.6 points\. Its 4\.2\-point deficit to Phase\-Revised is only two successful attempts\. The decisive downstream distinction is therefore witness source: both no\-feedback sources outperform the feedback\-loop source, while the aggregate results do not establish a Phase\-Revised advantage over Direct\-Revised\. The True\-Spec reference is 10\.4 points above Phase\-Revised and 14\.6 above Direct\-Revised, indicating remaining headroom in the repair\-and\-synthesis workflow without identifying a unique cause for that gap\.

Phase\-Revised reaches39/44=88\.6%39/44=88\.6\\%of the True\-Spec success count\. The four unsuccessful True\-Spec attempts show that restoring the intended contract does not eliminate synthesis difficulty\. These are attempt counts, not an upper bound on what another run or model could achieve\.

### 4\.7\. Held\-out oracle check and benchmark extension

In a separate oracle check, two cases per task are withheld from the certification disagreement criterion\. Among visible\-certified witnesses, 79/85Directwitnesses \(92\.9%\), 36/39IntentShieldwitnesses \(92\.3%\), and 78/85Phasewitnesses \(91\.8%\) also disagree on at least one withheld case\. The witness evidence extends beyond visible selection cases for the overwhelming majority of certified outcomes\. The sixDirectwitnesses without withheld\-case disagreement are not invalidated: each already exhibits an official counterexample under the certification protocol\. The 92\.9% conditional rate is not an estimate of selection\-oracle inflation or universal input\-space coverage; restored\-contract failure remains a separate gate\.

An eight\-task extension yields 49/96 witnesses forDirect\(51\.0%\) and 21/96 forIntentShield\(21\.9%\)\. Combined with the primary matrix, the 20\-task totals are 134/240 versus 60/240, a 30\.8\-point difference \(task\-bootstrapp=0\.0018p=0\.0018\)\. These extension results are preliminary; the fixed 12\-task matrix remains the primary inferential study\.

### 4\.8\. The effect did not reproduce in transfer evaluations

In the available Dafny experiments, frontier routes were at ceiling and the Qwen stratum with limited headroom slightly favoredIntentShieldoverDirect\(23/24 versus 21/24\)\. On 24 Lean tasks from Verina\[[5](https://arxiv.org/html/2610.20676#bib.bib5)\],Phaseis the lowest arm: it solves 8 of 48 cells, compared with 12 forDirectand 14 for bothIntentShieldand a no\-context control\. The LeanDirect\-minus\-Phasedifference is 8\.3 points \(task\-bootstrap 95% interval \[−4\.2\-4\.2, 20\.8\],p=0\.31p=0\.31\), which does not establish a repeat\-run difference\. Dafny’s high success rates limit headroom, while Lean’s full\-function and tactic\-proof setting differs from expression\-level Verus search\. These are possible explanations, not evidence of positive transfer\. Appendix[E](https://arxiv.org/html/2610.20676#A5)shows the complete transfer summary\.

## 5\. Discussion and limitations

#### What the controls establish\.

The Verus result is not explained away by protocol structure or broken syntax\.FMIretains the iterative protocol while removing the full compiler/verifier/test feedback block; the resulting 22\.2\-point improvement accounts for the larger share of the observedDirect–IntentShieldgap\. Prompt length remains matched within 3%\. Parser repair retains a 27\.1\-point advantage, so formatting failures cannot account for the full discovery penalty\. These are controlled policy contrasts: they establish the cost of introducing semantic feedback into this workflow without isolating individual feedback channels or internal model mechanisms\.

#### Empirical boundary\.

The primary benchmark contains 12 competitive\-programming functions and a restricted expression language; the 20\-task extension is preliminary\. Task\-cluster resampling retains within\-task dependence but cannot remove benchmark\-selection effects or guarantee robustness to provider\-wide drift\. Provider defaults and non\-seeded repeat labels limit exact replay\. The effect did not reproduce in the available Dafny or Lean evaluations\. The demonstrated failure mode is therefore a result about the studied Verus/Rust substrate and task class, not a universal property of feedback\. Repositories, mutable state, concurrency, and other proof workflows remain outside the evaluated scope\.

#### Task difficulty and downstream scope\.

Residual\-contract tasks favorDirectby 38\.3 points, compared with 27\.4 on total\-omission controls\. The latter can admit constants such as0ortrue, so they probe harness reliability as well as semantic search\. Even an easy omitted relation requires a parsable, compilable candidate that verifies and disagrees with intended behavior\. Direct\-Revised is a witness\-guided control, not specification strengthening without a witness\. The three low\-yield IS\-Revised cases use best\-available candidates, potentially uncertified, so its downstream deficit combines discovery, selection, and repair effects rather than isolating repair quality\. True\-Spec is an empirical oracle reference, not a proven upper bound on stochastic synthesis\.

#### Why Verus may differ\.

Rust typing, ownership, and arithmetic obligations provide a rich correction surface: feedback can make an expression more acceptable to the verifier while steering it toward intended behavior\. Dafny’s different type discipline and Lean’s tactic\-based proof setting may change this interaction\. These are substrate\-specific hypotheses, not measured mediators\. The observed transfer directions favorIntentShieldby 8\.3 points in the Dafny Qwen stratum and by 4\.2 points in Lean; they delimit the claim rather than corroborating it\.

#### Deployment consequence\.

The experiments deliberately weaken research contracts; witnesses expose missing obligations, not deployed runtime exploits\. Certification requires the restored intended postcondition and an oracle\. The handoff must retain the witness and checker evidence, route them to contract repair, and check the repaired specification against intended examples\. As with fuzzer findings, the specification author must triage the missing obligation before changing code or contracts\. A pre\-merge CI check should restrict reports to the owning team and reviewers\. Public specifications also exist, so access restrictions are deployment safeguards, not inherent properties of witness search\.

## 6\. Related work

Verus and VeriContest study verified Rust generation\[[3](https://arxiv.org/html/2610.20676#bib.bib3),[1](https://arxiv.org/html/2610.20676#bib.bib1)\]; Verina and VerifyThisBench evaluate generation of programs, specifications, and proofs\[[5](https://arxiv.org/html/2610.20676#bib.bib5),[7](https://arxiv.org/html/2610.20676#bib.bib7)\]\. Agentic and recursive systems generally optimize proof completion\[[9](https://arxiv.org/html/2610.20676#bib.bib9),[11](https://arxiv.org/html/2610.20676#bib.bib11),[13](https://arxiv.org/html/2610.20676#bib.bib13)\]\. Our objective is different: find a program admitted by an incomplete proof boundary\. VeriContest’s negative tests already target postcondition completeness; we complement that evaluation by studying how discovery policies preserve or suppress concrete witnesses and how those witnesses support subsequent repair\.

Recent work distinguishes faithful intent formalization from verifier acceptance\[[15](https://arxiv.org/html/2610.20676#bib.bib15),[17](https://arxiv.org/html/2610.20676#bib.bib17),[19](https://arxiv.org/html/2610.20676#bib.bib19)\]\. Conventional counterexample\-guided synthesis removes failing candidates\[[21](https://arxiv.org/html/2610.20676#bib.bib21),[23](https://arxiv.org/html/2610.20676#bib.bib23)\]; completeness auditing must preserve the admitted failure long enough to identify the missing obligation\. This connects to specification gaming\[[25](https://arxiv.org/html/2610.20676#bib.bib25),[27](https://arxiv.org/html/2610.20676#bib.bib27),[29](https://arxiv.org/html/2610.20676#bib.bib29)\]and complements self\-refinement methods that optimize ordinary task performance\[[31](https://arxiv.org/html/2610.20676#bib.bib31)\]\.

Related studies examine whether verifier\-side information changes an agent’s effective decision rather than merely appearing in its context\. ParetoProof studies Pareto selection in Lean proof maintenance\[[4](https://arxiv.org/html/2610.20676#bib.bib4)\]; process\-credit auditing studies whether scores steer verifier\-guided repair\[[12](https://arxiv.org/html/2610.20676#bib.bib12)\]\. ProofDebt examines checker\-backed memory in continual software repair and distinguishes tasks that need earlier information from those that do not\[[20](https://arxiv.org/html/2610.20676#bib.bib20)\]\. Here the information is correctness feedback, and the outcome is preservation of a specification\-completeness witness: the matched iterative control tests its contribution under a fixed discovery protocol\. These preprints concern related control and information\-use questions, not independent replications of the Verus result\.

## 7\. Conclusion

Our experiments establish a failure mode of verifier\-guided completeness auditing: a correctness\-oriented discovery loop suppresses the admitted wrong programs it is supposed to find\. In the studied Verus/Rust workflow, corrective feedback cuts certified\-witness yield from 59\.0% to 27\.1%, discarding more than half the yield available under the same call budget\. The matched iterative control places 69\.6% of the observed gap in the feedback\-content contrast, not independent restarts\. Every model family favors no\-feedback discovery, parser repair leaves a 27\.1\-point gap, and 92\.9% ofDirect\-certified witnesses also expose held\-out disagreements\. This is a large, cross\-family discovery penalty that survives both protocol and syntax checks within the evaluated Verus task class\.

Preserving the evidence has a concrete downstream payoff\. Phase\-Revised specifications raise implementation success from 29\.2% under weakened contracts to 81\.3%, and exceed IS\-Revised’s 62\.5% without losing on any downstream task\. Direct\-Revised reaches 77\.1%, establishing that both no\-feedback witness sources deliver stronger contract repair\. Phase separation turns preservation into an explicit, auditable handoff: discover the failure, freeze the candidate, certify the missing obligation, and only then introduce correctness\-oriented repair\.

The negative Dafny and Lean results define the empirical boundary, not a reversal of the Verus evidence\. Combining completeness auditing with correctness repair incurs a measured cost here\. The operational prescription for this Verus workflow is unambiguous: preserve the counterexample before correcting it\. A verifier’s acceptance is not a completeness certificate; the admitted wrong program is the evidence needed to strengthen the specification\.

## References

- \[1\]Zichen Xie, Mrigank Pawagi, Yuxin Liu, Aaditi Rai, Lize Shao, John Berberian, Sicong Che, and Wenxi Wang\.Vericontest: A competitive\-programming benchmark for verifiable code generation\.*arXiv preprint arXiv:2605\.08553*, 2026\.
- \[2\]Shashank Indukuri and Adarsh Agrawal\.Grounded optimization: A layered engineering framework for reducing llm hallucination in automated personal document rewriting\.*arXiv preprint arXiv:2607\.01457*, 2026\.
- \[3\]Andrea Lattuada et al\.Verus: Verifying rust programs using linear ghost types\.*Proceedings of the ACM on Programming Languages*, 7\(OOPSLA1\), 2023\.doi:10\.1145/3586037\.
- \[4\]Adarsh Agrawal\.ParetoProof: When does pareto selection improve Lean proof maintenance?*Preprints\.org*, 2026a\.doi:10\.20944/preprints202610\.0407\.v1\.URL[https://www\.preprints\.org/manuscript/202610\.0407](https://www.preprints.org/manuscript/202610.0407)\.Preprint, version 1\.
- \[5\]Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song\.VERINA: Benchmarking verifiable code generation\.*arXiv preprint arXiv:2505\.23135*, 2025\.
- \[6\]AAG Intelligence\.Amazon nova multimodal embeddings: Technical report and model card\.Technical report, Amazon, 2025a\.
- \[7\]Xun Deng, Sicheng Zhong, Barış Bayazıt, Andreas Veneris, Fan Long, and Xujie Si\.Verifythisbench: Generating code, specifications, and proofs all at once\.*arXiv preprint arXiv:2505\.19271*, 2025\.
- \[8\]Adarsh Agrawal and Rahul Suresh Babu\.Incident memory: Training\-free operational memory through sequential pattern mining and velocity\-stratified retrieval\.*arXiv preprint arXiv:2609\.01616*, 2026\.
- \[9\]Pranjal Aggarwal, Bryan Parno, and Sean Welleck\.Alphaverus: Bootstrapping formally verified code generation through self\-improving translation and treefinement\.*arXiv preprint arXiv:2412\.06176*, 2024\.
- \[10\]Bertie Vidgen, Adarsh Agrawal, A\. M\. Ahmed, V\. Akinwande, N\. Al\-Nuaimi, N\. Alfaraj, et al\.Introducing v0\.5 of the ai safety benchmark from mlcommons\.*arXiv preprint arXiv:2404\.12241*, 2024a\.
- \[11\]Benjamin Breen, Austin Letson, Borja Requena Pozo, and Leopoldo Sarra\.Axdafny: Agentic verified code generation in dafny\.*arXiv preprint arXiv:2606\.32007*, 2026\.
- \[12\]Adarsh Agrawal\.When scores do not steer: Auditing process credit in verifier\-guided repair\.*Preprints\.org*, 2026b\.doi:10\.20944/preprints202610\.0363\.v1\.URL[https://www\.preprints\.org/manuscript/202610\.0363](https://www.preprints.org/manuscript/202610.0363)\.Preprint, version 1\.
- \[13\]Max Tan\.Automating formal verification with reinforcement learning and recursive inference\.*arXiv preprint arXiv:2605\.30914*, 2026\.
- \[14\]AAG Intelligence\.Amazon nova sonic: Technical report and model card\.Technical report, Amazon, 2025b\.
- \[15\]Shuvendu K\. Lahiri\.Intent formalization: A grand challenge for reliable coding in the age of ai agents\.*arXiv preprint arXiv:2603\.17150*, 2026\.
- \[16\]Adarsh Agrawal and Shashank Indukuri\.Schema\-first retrieval: Embedding catalogs for natural language analytics\.*arXiv preprint arXiv:2606\.28387*, 2026\.
- \[17\]Zhe Ye, Aidan Z\. H\. Yang, Huangyuan Su, Zhenyu Liao, Samuel Tenka, Zhizhen Qin, Udaya Ghai, Dawn Song, and Soonho Kong\.Intent\-aligned formal specification synthesis via traceable refinement\.*arXiv preprint arXiv:2604\.10392*, 2026\.
- \[18\]AAG Intelligence\.Amazon nova premier: Technical report and model card\.Technical report, Amazon, 2025c\.
- \[19\]Md Rakib Hossain Misu, Iris Ma, and Cristina V\. Lopes\.Veriact: Beyond verifiability – agentic synthesis of correct and complete formal specifications\.*arXiv preprint arXiv:2604\.00280*, 2026\.
- \[20\]Adarsh Agrawal\.ProofDebt: When does memory improve continual software repair?*Preprints\.org*, 2026c\.doi:10\.20944/preprints202610\.0373\.v1\.URL[https://www\.preprints\.org/manuscript/202610\.0373](https://www.preprints.org/manuscript/202610.0373)\.Preprint, version 1\.
- \[21\]Armando Solar\-Lezama, Rodric Rabbah, Rastislav Bodik, and Kemal Ebcioglu\.Programming by sketching for bit\-streaming programs\.In*Proceedings of PLDI*, 2005\.
- \[22\]Rahul Suresh Babu and Adarsh Agrawal\.Self\-healing agentic orchestrators for reliable tool\-augmented large language model systems\.*arXiv preprint arXiv:2606\.01416*, 2026\.
- \[23\]Rajeev Alur et al\.Syntax\-guided synthesis\.In*Proceedings of FMCAD*, 2013\.
- \[24\]AAG Intelligence\.Amazon nova 2: Multimodal reasoning and generation models\.Technical report, Amazon, 2025d\.
- \[25\]Dario Amodei et al\.Concrete problems in ai safety\.*arXiv preprint arXiv:1606\.06565*, 2016\.
- \[26\]Wei Feng, Adarsh Agrawal, Haifeng Ling, Erik Blasch, E\. Adiles\-Cruz, P\. T\. Schrader, and J\. Wei\.DDDAS probability learning for natural disaster change detection\.In*International Conference on Dynamic Data Driven Applications Systems*, pages 90–99, 2024\.
- \[27\]Jan Leike et al\.Ai safety gridworlds\.*arXiv preprint arXiv:1711\.09883*, 2017\.
- \[28\]Bertie Vidgen, Adarsh Agrawal, A\. M\. Ahmed, V\. Akinwande, N\. Al\-Nuaimi, N\. Alfaraj, et al\.How to construct ai safety benchmarks, 2024b\.
- \[29\]Kei Nishimura\-Gasparian, Robert McCarthy, and David Lindner\.Towards understanding specification gaming in reasoning models\.*arXiv preprint arXiv:2605\.02269*, 2026\.
- \[30\]Adarsh Agrawal and J\. Li\.Mitigating bias in ai using debias\-gan\.NVIDIA GTC Conference, 2022\.
- \[31\]Aman Madaan et al\.Self\-refine: Iterative refinement with self\-feedback\.In*Advances in Neural Information Processing Systems*, 2023\.
- \[32\]A\. V\. Adarsh Agrawal and Nikhil Garg\.Time series forecasting of producer price index, using arima\.*International Journal of Science and Research \(IJSR\)*, 7\(7\):1019–1024, 2018\.
- \[33\]AAG Intelligence\.The amazon nova family of models: Technical report and model card\.Technical report, Amazon, 2024\.

## Appendix AModel routes and generation settings

The primary campaign ran in September 2026\. Runtime and inference\-profile calls used Amazon Bedrock inus\-west\-2; Terra used the Bedrock Mantle Responses route\. Table[A1](https://arxiv.org/html/2610.20676#A1.T1)records the identifiers used in the reported campaigns and auxiliary cross\-family diagnostics\.

Table A1:Model identifiers and campaign roles\. The first four models form the primary discovery matrix; downstream settings appear in Appendix D\.Optional decoding fields were not overridden\. Claude Sonnet 5 and Opus 5 used adaptive thinking with the provider\-default high effort and no temperature parameter\. DeepSeek V3\.2, Devstral 2, Qwen3\-Coder, GLM\-5, and MiniMax M2\.5 used their Runtime provider defaults for temperature, top\-pp, top\-kk, and stopping behavior\. These defaults are identified by model and invocation month because provider defaults may evolve\. Every method used three calls per episode; failed parses were retained as failures\.

## Appendix BPrompt templates

The templates below use braces for task\-specific fields\. Line wrapping and punctuation are normalized for print\.IntentShieldcall 1, Model\-Judgment call 1,FMIcall 1, and everyPhasecall use theDirecttemplate\.

#### Directsystem prompt\.

```
You are an expert in formal verification and adversarial testing.
Your task is to expose incomplete formal specifications by finding
programs that satisfy a weakened formal contract while violating the
intended behavior described in natural language.

Your goal is NOT to implement the task correctly. Your goal is to find
a concrete example that exposes a gap between what the contract
verifies and what the task actually requires.
```

#### Directuser prompt\.

```
Task Description:
{natural_language_task}

Weakened Verus Contract:
{weakened_contract_code}

The contract has been deliberately weakened. Find a concise pure Rust
expression that:
1. Verifies successfully under this weakened contract.
2. Violates the intended behavior described in the task.

Known-Wrong Mutation Examples:
{mutation_examples}

Use these as guidance for specification gaps to explore.
Constraints:
- Return a pure Rust expression only.
- No statements, loops, unsafe blocks, I/O, or macros.
- Be deterministic and parse as valid Rust syntax.
- Prefer concise expressions.

Tracking Label: {replicate_label}
Respond with ONLY the candidate expression.
```

#### IntentShieldcalls 2 and 3\.

```
Task Description: {natural_language_task}
Weakened Verus Contract: {weakened_contract_code}
Previous Candidate: {previous_expression}

Feedback from Previous Round:
- Rust Compilation: {rustc_status}
- Weakened Contract Verification: {verus_weakened_status}
- Visible Test Results: {visible_test_table}
- Pass: {num_pass}/{num_visible}
- Fail: {num_fail}/{num_visible}

Find a program that the weakened contract admits but the intended task
behavior rejects. If the candidate failed to compile or verify, revise
it to pass both gates. If it passes the contract but fails visible
tests, consider preserving that failure mode.

Tracking Label: {replicate_label}
Respond with the revised candidate expression.
```

#### FMIcalls 2 and 3\.

Use the same preceding\-candidate template and output instruction asIntentShield\. Replace the complete compiler, verifier, and test\-results block with:

```
Feedback from Previous Round:
compilation: [not evaluated]
verification: [not evaluated]
tests: [not evaluated]
```

Prompt length is matched to within 3%\. This preserves the iterative structure and does not add “ONLY” to the output instruction\. The separateIntentShieldkeyword control changes only that output instruction to require the candidate expression only\.

#### Model\-Judgment calls 2 and 3\.

```
Task Description: {natural_language_task}
Weakened Verus Contract: {weakened_contract_code}
Previous Candidate: {previous_expression}

Assess the previous candidate:
1. Does it verify under the weakened contract?
2. Does it violate the intended task behavior?
3. Is it a valid specification-completeness witness?

Provide the assessment, then revise the candidate if needed.
Tracking Label: {replicate_label}
Format:
Assessment:
Revised Candidate:
```

#### A2 specification repair\.

The witness field contains the selected candidate from the corresponding discovery policy\. For three low\-yield IS\-Revised tasks it is the highest\-ranked available candidate and may be uncertified; the template label does not confer certification\. Direct\-Revised and Phase\-Revised use their respective certified witnesses\.

```
Task Description: {natural_language_task}
Current Weakened Contract: {weakened_contract_code}
Certified Witness: {witness_expression}

Test Failure Evidence:
Input: {failing_test_input}
Expected Output: {expected_output}
Witness Output: {witness_actual_output}

Propose a minimal contract strengthening that rejects this witness and
similar wrong behaviors, preserves intended correct implementations,
and adds only necessary postconditions. Return the complete repaired
Verus function signature with ensures clauses.
```

#### A2 implementation synthesis\.

```
Task Description: {natural_language_task}
Formal Verus Contract: {specification_code}
Official Test Cases (visible): {visible_test_cases}

Synthesize a pure Rust expression that satisfies the contract and
passes all visible test cases. Return only the implementation
expression.
```

## Appendix CTask\-level Verus results

Table A2:Task\-level discovery counts and omitted properties\. Each policy contributes 12 outcomes per task\. Primary inference compares Direct andIntentShield; Model\-Judgment is secondary\.Phasealso totals 85/144, with matching task totals on 10 of 12 tasks\.cf47Aandcf486Aeach differ fromDirectby one outcome in opposite directions\. Table[A5](https://arxiv.org/html/2610.20676#A7.T5)reports the paired\-cell contingency table rather than equating aggregate totals with identical cells\.

## Appendix DDownstream task results

Across all five conditions, Claude Sonnet 5 makes three independent implementation attempts per task using the same specification, without carry\-over between attempts\. Sonnet uses adaptive thinking with default high effort\. Optional temperature and sampling controls are not overridden\. The model routes are listed in Table[A1](https://arxiv.org/html/2610.20676#A1.T1)\.

Direct\-Revised usesDirect\-discovered certified witnesses; it is not a witness\-free strengthening baseline\. True\-Spec bypasses specification repair and supplies the intended contract directly\. Their aggregate results are 37/48 \(77\.1%\) and 44/48 \(91\.7%\), respectively, versus 39/48 \(81\.3%\) for Phase\-Revised, 30/48 \(62\.5%\) for IS\-Revised, and 14/48 \(29\.2%\) for Original\.

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\.
## Appendix ETransfer and mechanism diagnostics

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](https://arxiv.org/html/2610.20676#S4.T2)is a separate post\-hoc analysis\.
## Appendix FRepresentative certified witnesses

Table A4:Examples of programs admitted by a weakened contract but rejected by the restored obligation and an official case\.
## Appendix GAdditional diagnostic results

Table A5:IndependentDirect/Phaseexecutions on 144 paired cells\. Equal totals arise from fresh generation, not identical successful cells\.Agreement is122/144=84\.7%122/144=84\.7\\%; chance agreement from the observed marginals ispe=\(85/144\)2\+\(59/144\)2p\_\{e\}=\(85/144\)^\{2\}\+\(59/144\)^\{2\}\. Thusκ=\(122/144−pe\)/\(1−pe\)=0\.6841\\kappa=\(122/144\-p\_\{e\}\)/\(1\-p\_\{e\}\)=0\.6841, rounding to 0\.68\. Of 74 co\-certified witnesses, 31 are string\-identical and 43 are distinct, independently certified expressions\. Each execution also certifies 11 unique cells\.

Table A6:Held\-out oracle diagnostic using two withheld cases per task\. Rates are conditional on visible certification, not all discovery episodes\.Held\-out disagreement supplies additional counterexamples, not distribution\-wide coverage\. SixDirect, threeIntentShield, and sevenPhasewitnesses fail official cases but not these two withheld cases; this does not establish their correctness\.

Table A7:Task\-stratum yields\. Total omissions admit simple constants; residual contracts retain meaningful output obligations\.The larger residual\-contract gap rules out an effect confined to trivial omissions\. Total\-omission witnesses must still pass parsing, typing, arithmetic\-safety, and verifier gates before exhibiting wrong behavior\.

Table A8:Benchmark extension\. The eight\-task extension and combined results are preliminary; the original 12\-task matrix is the primary analysis\.[1](https://arxiv.org/html/2610.20676#bib.bib1),[2](https://arxiv.org/html/2610.20676#bib.bib2),[3](https://arxiv.org/html/2610.20676#bib.bib3),[4](https://arxiv.org/html/2610.20676#bib.bib4),[5](https://arxiv.org/html/2610.20676#bib.bib5),[6](https://arxiv.org/html/2610.20676#bib.bib6),[7](https://arxiv.org/html/2610.20676#bib.bib7),[8](https://arxiv.org/html/2610.20676#bib.bib8),[9](https://arxiv.org/html/2610.20676#bib.bib9),[10](https://arxiv.org/html/2610.20676#bib.bib10),[11](https://arxiv.org/html/2610.20676#bib.bib11),[12](https://arxiv.org/html/2610.20676#bib.bib12),[13](https://arxiv.org/html/2610.20676#bib.bib13),[14](https://arxiv.org/html/2610.20676#bib.bib14),[15](https://arxiv.org/html/2610.20676#bib.bib15),[16](https://arxiv.org/html/2610.20676#bib.bib16),[17](https://arxiv.org/html/2610.20676#bib.bib17),[18](https://arxiv.org/html/2610.20676#bib.bib18),[19](https://arxiv.org/html/2610.20676#bib.bib19),[20](https://arxiv.org/html/2610.20676#bib.bib20),[21](https://arxiv.org/html/2610.20676#bib.bib21),[22](https://arxiv.org/html/2610.20676#bib.bib22),[23](https://arxiv.org/html/2610.20676#bib.bib23),[24](https://arxiv.org/html/2610.20676#bib.bib24),[25](https://arxiv.org/html/2610.20676#bib.bib25),[26](https://arxiv.org/html/2610.20676#bib.bib26),[27](https://arxiv.org/html/2610.20676#bib.bib27),[28](https://arxiv.org/html/2610.20676#bib.bib28),[29](https://arxiv.org/html/2610.20676#bib.bib29),[30](https://arxiv.org/html/2610.20676#bib.bib30),[31](https://arxiv.org/html/2610.20676#bib.bib31),[32](https://arxiv.org/html/2610.20676#bib.bib32),[33](https://arxiv.org/html/2610.20676#bib.bib33)