Badania zespołu naukowego ujawniają kontraintuicyjny wynik w testowaniu modeli języka do audytu specyfikacji programów: system informacji zwrotnej IntentShield, mający poprawiać błędy, faktycznie hamuje odkrywanie rzeczywistych problemów. Gdy model pracuje bez sprzężenia zwrotnego, znajduje ponad dwa razy więcej świadków certyfikowanych niezgodności specyfikacji w programach Verus/Rust - 59% wobec 27% w pętli korygowania.
Klucz do tego efektu leży w konflikcie celów: audyt kompletności specyfikacji ma znaleźć programy, które formalnie spełniają kontrakt, ale naruszają prawdziwe zamiary projektanta. Kiedy model otrzymuje informacje zwrotne o błędach i próbuje je naprawić, zaczyna generować kody bardziej zgodne z negatywną informacją zwrotną, co podtłumia przypadki niezgodności. Format iteracyjny z fazą niezależnego odkrywania i osobną fazą wykonania nie tylko utrzymał 59% wyjściowych wyników, ale umożliwił uzyskanie 81% sukcesu w naprawie specyfikacji - znacznie lepiej niż 62,5% przy bezpośredniej korekcji.
Autorzy testowali to na 12 zadaniach Verus/Rust w czterech rodzinach modeli i zaproponowali nowy paradygmat: zamiast natychmiastowo korygować błędy, najpierw należy je zachować, certyfikować i badać jako dowody niekompletności specyfikacji. Efekt nie pojawia się w testach z Dafnym i Lean, co sugeruje, że jest specyficzny dla przepływu pracy Verus/Rust. Rezultaty kształtują praktyczne implikacje dla bezpieczeństwa oprogramowania.