명세 완전성 감사는 작성된 계약은 만족하지만 의도된 동작은 어기는 프로그램을 찾아내려 하지만, 정답 여부에 대한 교정 피드백은 바로 그 증거를 지워버린다는 역설이 있다. 연구팀은 4개 모델군, 12개 Verus/Rust 과제에서 이를 입증했는데, 피드백 없는 독립 탐색이 IntentShield의 교정 피드백 루프보다 인증된 반증 수율을 두 배 이상(59.0% 대 27.1%) 높였다. 형식을 맞춘 반복 대조군을 통해 이 차이가 독립 재시작이 아니라 피드백 내용 자체에서 비롯됨을 보였고, 모든 모델군에서 일관되게 나타났으며 파서 복구 후에도 유지됐다. 위상 분리 실행으로 응답 재사용 없이 같은 수율을 재현했고, 이렇게 보존된 반증을 활용하면 명세 복구 성공률이 81.3%(위상 복구)로 IntentShield 복구(62.5%)보다 훨씬 높아졌다(Dafny·Lean에서는 재현되지 않음).

• •'정답 피드백'이 계약은 만족하지만 의도는 어기는 반증 프로그램을 발견하는 능력을 오히려 억제함을 실증
• •피드백 없는 독립 탐색이 IntentShield 교정 루프 대비 인증 반증 수율 2배 이상(59.0% 대 27.1%)
• •위상 분리(완전성 감사 먼저, 교정 나중) 전략이 명세 복구 성공률을 81.3%까지 끌어올림
• •효과는 Verus/Rust에서만 확인, Dafny·Lean 평가에서는 재현되지 않아 경계가 뚜렷함