[Stanford CS146S #9] 자율 TDD와 형식 검증: Z3 SMT 솔버, 속성 기반 불변식, AI 생성 코드의 수학적 증명
· 약 8분
스탠포드 대학교(Stanford University) CS146S: The Modern Software Developer(현대 소프트웨어 개발자) 기술 분석 시리즈 아홉 번째 시간입니다.
우리는 지금까지 프롬프트 엔지니어링(2강), Model Context Protocol(MCP) 도구 연동(3강), 자가 치유형 CI 하네스(4강), 다중 에이전트 스웜(5강), eBPF 런타임 추적(6강), AST 린터와 오염 분석(7강), 그리고 AI 네이티브 아키텍처(8강)를 다루었습니다.
이번 9강에서는 현대 AI 소프트웨어 엔지니어링이 마주한 가장 궁극적인 질문을 던집니다: "비결정론적이고 확률적인 파운데이션 모델이 작성한 코드를 어떻게 금융, 항공우주, 암호학, 분산 시스템 같은 미션 크리티컬 프로덕션 환경에 100% 신뢰하고 배포할 수 있는가?"
50여 년 전 컴퓨터 과학의 선구자 에츠허르 다익스트라(Edsger Dijkstra)는 이렇게 갈파했습니다: "프로그램 테스트는 버그가 존재함을 증명할 수는 있어도, 버그가 없음을 증명할 수는 없다!" 이번 강의에서 스탠포드 연구진은 단순한 예제 기반 단위 테스트를 넘어, 자율 속성 기반 테스트(Property-Based Testing, PBT), 기호 실행(Symbolic Execution), 그리고 **Z3 SMT(Satisfiability Modulo Theories) 솔버를 통한 형식 검증(Formal Verification)**으로 이어지는 수학적 무결성 검증 체계를 공개합니다.