Zstd와 IMAP 구현을 대상으로 여러 검증 기법을 반복 비교한 결과, 에이전트는 TLA+ 모델 160개 중 159개를 만들고도 실제 Rust 수정으로 연결하지 못했고 TDD는 테스트 수만 늘린 채 어려운 사례를 자주 놓쳤습니다. 구조화된 무작위 입력은 드물었지만 절반에서 실제 버그를 찾았고, 긴 테스트 스킬은 비용을 최대 41% 높여도 정확도를 개선하지 못했습니다. 가장 나은 지시는 예상 실수와 경계 양쪽을 먼저 식별하는 짧은 맞춤형 절차였습니다.