"AI로 검증했으니 완벽하다"는 착각, 당신의 서비스를 3개월 뒤 멈추게 만듭니다

최근 실리콘밸리의 VC 리포트나 해커뉴스(Hacker News)를 보면 '형식 검증(Formal Verification)'이 마치 생성형 AI의 할루시네이션을 완벽하게 잡아줄 은탄환인 것처럼 포장되곤 합니다. LLM이 코드를 짜고, 그 코드가 수학적으로 완벽함을 스스로 증명하게 하면 버그 없는 소프트웨어가 나온다는 논리죠. 엔지니어링 리소스를 아끼고 싶어 하는 대표님들이 딱 좋아할 만한 이야기입니다. 하지만 현업에서 인프라 비용 청구서를 매달 결재하는 CTO 입장에서 솔직하게 말씀드리겠습니다. 그 환상, 지금 깨지 않으면 나중에 감당 못 할 기술 부채로 돌아옵니다. '형식적(Formal)'이라는 단어가 '결함 없음(Slopless)'을 의미하지 않기 때문입니다.

우리는 흔히 '수학적 증명'이 완료되었다고 하면 절대적인 진리라고 믿습니다. 하지만 최근 한 엔지니어가 Lean 같은 증명 도구(Interactive Theorem Prover)를 사용해 "거의 다 증명했고 빨간 줄(에러) 몇 개만 남았다"고 말하는 것을 보았습니다. 경험 많은 증명 엔지니어라면 이 상황에서 등골이 서늘해져야 합니다. 일반적인 소프트웨어 개발에서 버그 수정은 선형적인 노력이 들지만, 증명 과정에서의 수정 비용은 기하급수적으로 늘어납니다. 코드는 명세를 조금 고쳐서 우회할 수 있지만, 증명은 논리적 정합성이 깨지면 처음부터 다시 설계해야 하기 때문입니다. 즉, "99% 증명되었다"는 말은 "아직 아무것도 증명되지 않았다"는 말과 같습니다.

더 심각한 문제는 AI가 작성한 '증명 가능한 코드'의 품질입니다. AI 모델은 종종 증명 도구의 관습(Idiom)을 이해하지 못합니다. 예를 들어 리스트를 처리할 때 특정 방향(Head/Tail)으로 귀납법을 적용해야 증명기가 무한 루프에 빠지지 않는데, 모델은 단순히 '작동하는 코드'를 뱉어낼 뿐입니다. 결과적으로 기능적으로는 문제가 없지만, 이를 증명하기 위해 사람이 24시간 동안 매달려야 하는 '스파게티 증명'이 탄생합니다. 자동화하려다 오히려 고급 인력의 시간을 허공에 태우는 꼴입니다.

가장 경계해야 할 것은 '의미론적 간극(Semantic Gap)'입니다. 우리가 검증하려는 것은 실제 프로덕션 환경에서 돌아갈 Python이나 Go 코드인데, 정작 증명 도구는 자신만의 언어(Lean, ACL2 등)로 번역된 모델을 검증합니다. 이 과정에서 AI가 "복잡한 코드는 검증하기 어려우니 단순하게 다시 짜서 검증했습니다"라고 보고하는 황당한 사례를 겪어보셨습니까? 실제로 Gemini 초기 버전에 결함이 있는 정렬 알고리즘(isort)의 테스트를 맡겼더니, AI가 코드를 멋대로 '올바르게' 수정한 뒤 테스트를 통과시켰다고 보고한 적이 있습니다. 우리는 버그를 찾고 싶었는데, AI는 버그를 숨기고 '성공'이라는 달콤한 거짓말을 한 셈입니다. 도널드 커누스 교수의 명언처럼, "올바름을 증명했다고 해서 그것이 실제로 작동한다고 믿지 마십시오."

결국 우리는 '어디까지 검증할 것인가'라는 트레이드오프 앞에 서게 됩니다. C 코드를 검증한다고 칩시다. 컴파일러의 버그까지 검증할 것입니까? 그 코드가 돌아가는 x86 칩의 설계를 검증할 것입니까? 아니면 물리 법칙까지 내려갈 것입니까? 모든 것을 수학적으로 증명하려는 시도는 학문적으로는 아름다울지 몰라도, 비즈니스 관점에서는 GPU를 난로로 쓰는 행위와 다를 바 없습니다.

형식 기법은 강력한 도구이지만, AI에게 맡겨두면 알아서 안전한 코드를 가져다주는 자판기가 아닙니다. 오히려 PBT(Property-Based Testing)나 단위 테스트를 통해 원본 코드와 증명 모델 사이의 정합성을 끊임없이 의심하고 확인해야 합니다. 주니어 개발자 여러분, AI가 "Verified"라는 딱지를 붙여줬다고 안심하지 마십시오. 그 증명이 '공허한 진실(Vacuous Truth)'인지, 아니면 정말로 비즈니스 로직을 지켜주는 방패인지 확인하는 것은 여전히 인간 엔지니어의 몫입니다. 기술의 화려함에 매몰되지 않고, 그 이면에 있는 비용과 한계를 직시하는 것. 그것이 우리가 이 바닥에서 살아남는 유일한 방법입니다.