OSDS: Contract-Bounded Verification of Effectful Generated Code Edits

Effectful generated-code edits intentionally change some behavior while other behavior should remain unchanged. Raw baseline--candidate equality can reject the intended change, while ordinary tests can miss a regression caused while computing it. OSDS checks a declared finite contract with separate conditions for requested-effect correctness and protected-behavior preservation. Its localization check requires baseline invariance, identical candidate bytes, and restoration of the protected behavior, and its evidence record is content-bound to the evaluated artifacts. In a frozen, mechanism-stratified controlled campaign of 100 scheduled coding-agent runs over 50 multi-file repositories, 99 runs produce candidates. All 99 candidates pass the original frozen public tests and hidden requested-effect checks; 34 fail protected stress preservation, with 20 failures in Agent A and 14 in Agent B. All 34 satisfy strict localization and retain requested-effect correctness under intervention. These counts characterize this benchmark, not provider-level defect rates. A six-check constraint experiment produces distinct invalid outcomes when individual OSDS checks are weakened. Eight constructed phenomenon-focused witnesses across seven pinned packages reproduce the mechanism class outside the controlled repositories. OSDS does not infer complete specifications or claim better detection than an oracle supplied with the same scenarios; it evaluates the stated contract and reports the resulting checks separately.