50년 후, 형식 검증에 반대하는 주장 재검토

The Case Against Formal Verification, 50 Years Later

AI 코딩의 부상으로 형식 검증에 대한 관심이 급증하고 있다. 1979년 논문 'Social Processes and Proofs of Theorems and Programs'은 형식 검증이 실패할 것이라고 주장했다. 이 글은 그 주장을 2026년의 관점에서 재검토한다. 저자는 검증이 수학적 증명과 같은 사회적 과정이 아니라는 점, 사양의 불완전성, 자동 검증의 한계, 실제 시스템의 복잡성 등 6가지 논거를 제시하며, 현대의 도구와 AI 에이전트의 등장으로 일부는 약화되었지만 여전히 유효한 점도 있다고 분석한다. 결론적으로 완전한 검증보다는 다양한 신뢰성 확보 방법이 중요하며, AI 코딩 시대에는 사양 작성과 검증이 더욱 중요해진다고 강조한다.