형식 검증(formal verification)은 오랫동안 극히 일부 영역에서나 쓸모 있는, 심하게는 시간 낭비로 취급받던 기술이었다. 그런데 최근 분위기가 달라졌다. 지난 2년 사이 '형식 검증'과 '형식 기법'에 대한 검색이 크게 늘었고, 많은 엔지니어가 증명 보조 도구인 Lean을 배우기 시작했으며, 새로운 명세 언어가 꾸준히 등장하고 있다. 시그널 앱을 전 구간(end-to-end)으로 검증하려는 Signal Shot 프로젝트처럼 실제 주요 애플리케이션을 통째로 검증하려는 시도도 나온다. Antithesis의 Will Wilson은 Bug Bash 2026 개막 강연 'We won, what now?'에서 이 틈새 분야의 승리를 선언하기도 했다.
이 관심의 핵심 동력은 AI 코딩이다. 이유는 세 가지로 정리된다. 첫째, AI 에이전트가 작성한 코드는 사람의 이해에 공백을 남기므로 별도의 정확성 확보 수단이 필요해진다. 둘째, AI는 검증 작업 자체를 빠르고 손쉽게 만들어 실제 개발 과정에 끼워 넣기 쉽게 한다. 셋째, 프로그램을 쓰는 일이 극도로 빨라지면 앞으로의 개선 여지는 결국 '정확성 보증' 쪽에 몰릴 수밖에 없다는 사업적 판단이다.
이런 낙관적 분위기 속에서, 원문 저자는 형식 검증에 반대한 1979년의 고전 논문 'Social Processes and Proofs of Theorems and Programs'를 다시 꺼내 든다. 이 논문은 '프로그램 검증은 실패할 수밖에 없으며, 그것이 누군가의 프로그램에 대한 확신에 영향을 줄 방법을 우리는 알 수 없다'고 단언했다. 다만 저자는 이 재검토가 완전히 진지한 결론이라기보다 흥미로운 사고 실험임을 분명히 한다. 논문이 겨냥한 것은 모든 형식 기법이 아니라 '완전 검증(full verification)'이며, 검증이 소프트웨어 공학의 일상이 될지도 아직 초기 신호에 불과하기 때문이다.
명세와 구현 사이의 간극
논문의 첫 번째 논지는 이렇다. 현실의 요구사항은 관계자들이 직관적으로 공유하는 비형식적인 것인데, 이를 형식 명세로 옮기는 과정 자체가 검증되지 않은 비형식적 작업이라 많은 것이 유실되거나 오해된다. 원문은 이를 타당한 지적으로 인정하면서도, 명세는 구현보다 비형식적 요구사항에 더 가깝기 때문에 오류를 발견하기가 오히려 쉽다고 반박한다. 나아가 Quint 같은 현대 명세 언어는 명세와 그 경계 사례들을 대화형으로 살펴볼 수 있어 직관과의 일치 여부를 확인하게 해 준다.
두 번째 논지는 명세가 구현과 독립적일 때만 가치를 갖는데, 반복적 개발 특성상 그 독립성 유지가 거의 불가능하며 결국 명세와 구현을 서로 끼워 맞추는 일이 된다는 것이다. 원문은 이 논거가 과거에도, 특히 코딩 에이전트가 개입하는 지금은 더욱 약하다고 본다. 추가로 얻는 이해는 개발 전반에 이롭고, 코드와 증명은 에이전트가 만들거나 바꿀 수 있지만 '무엇이 옳은가'를 규정하는 명세의 수정은 오직 인간이 최종 결정권자로서 맡는다는 역할 분담이 성립하기 때문이다.
완전 자동 검증기의 한계
논문은 사람 사이의 소통 수단으로서 검증이 부실하다고 본 뒤, 완전 자동 검증기라면 사정이 다를 수 있음을 인정하되 그런 도구는 만들어지기 어렵다고 봤다. 실제로 자동 검증기 개발은 진전이 있었으나 증명을 쓰거나 모델 검사용 모델을 만드는 사람의 노력은 여전히 핵심이다. 다만 LLM 기반 도구가 그 간극을 빠르게 좁히고 있다. Igor Konnov는 자신의 글에서 분산 프로토콜인 Ben-Or 프로토콜의 안전성을 Lean으로 증명한 경험을 소개하며, AI를 활용한 분산 프로토콜 증명이 생각보다 가까이 왔다고 전한다.
또한 논문은 'VERIFIED / NOT VERIFIED'만 답하는 검증기는 이해에 기여하지 못해 프로그래머를 막막하게 하고, 검증된 프로그램이 있으면 모니터링·속도 제한 같은 다른 방어 계층에 대한 동기를 줄인다고 우려했다. 원문은 이를 도구와 개발자 행태에 대한 최악의 가정에 기댄 약한 논거로 평가한다. 반면 알고리즘과 현실 시스템의 차이 지적에는 동의한다. 알고리즘 명세는 간결하지만 현실 시스템의 명세는 즉흥적이고 불안정하며 지저분하고, 대부분의 현실 시스템은 알고리즘 자체가 단순해 검증의 가치가 크지 않기 때문이다.
결국 모든 시스템을 검증할 필요는 없으며, 시스템 전체의 완전 검증이 신뢰성 확보의 최선인 경우도 드물다. 논문이 인용하듯, 검증을 만능으로 보는 시각은 수학 증명이나 공학 구조물이 채택하는 '현실적 정확성·신뢰성 기준', 즉 경제적 한계 안에서의 실현 가능성과 검증된 설계의 재활용, 동료 공동체에 대한 신뢰가 주는 이점을 가린다. 원문의 결론은 명료하다. 완전 검증에만 집중한 나머지 옛 저자들은 형식 기법의 부분적 활용이 이해와 설계, 개발 속도에 주는 이점을 과소평가했다는 것이다. AI 에이전트가 코드를 쓰고 인간이 '무엇을 만들지' 명세하고 '명세대로 만들어졌는지' 확인하는 구도에서, 검증은 에이전트가 스스로 옳게 짰는지 판단하며 루프를 닫는 수단이 된다. 검증은 다른 정확성 확보 노력과 경쟁하는 것이 아니라 함께 가는 선택지라는 점이 실무자가 새겨둘 대목이다.