소프트웨어의 버그는 대부분 테스트로 걸러낸다. 하지만 아무리 많은 입력을 던져봐도 "더 이상 버그가 없다"는 사실 자체를 증명하지는 못한다. 수십억 대의 기기에 올라가 가장 혹독하게 검증된 축에 드는 리눅스 커널조차 최근 1,000건이 넘는 취약점이 공개됐다. AI가 코드의 약점을 빠르게 찾아내 악용할 수 있게 된 지금, 기존의 방어 수단만으로는 부족하다는 문제의식에서 Anthropic과 Theorem의 이번 협업이 출발한다. 핵심 주장은 명확하다. 과거 극소수 고비용 프로젝트에만 쓰이던 정형 검증(formal verification)을, 대규모 언어모델을 이용해 훨씬 넓은 범위로 확장할 수 있게 됐다는 것이다.
왜 정형 검증은 비싸고 드물었나
정형 검증은 코드를 수학적 모델로 옮긴 뒤, 그 코드가 정해진 규칙(예: 메모리 안전성)을 어떤 입력에서도 어기지 않음을 증명하는 기법이다. 증명에 실패하면 그 실패 양상이 버그의 위치를 시사하고, 원인을 제거해 나가다 보면 결국 해당 규칙을 위반하는 버그가 없음을 보장하는 증명에 도달한다. 문제는 비용이다. 증명문은 원본 코드보다 몇 배나 커지고, 작성에는 고도로 전문화된 희소한 기술이 필요하다. 원문이 든 사례를 보면 seL4 운영체제 커널은 구현에 2인년이 들었지만 정형 검증에는 20인년이 소요됐다. 그래서 이 기법은 에어버스 항공전자 코드처럼 실패가 치명적인 분야에만 제한적으로 쓰여 왔다.
퍼즈 테스트를 명세로 바꾸는 방식
이번 작업의 영리한 지점은 "무엇이 올바른 동작인가"를 사람이 새로 정의하지 않았다는 데 있다. 텍스트 편집기나 브라우저의 '정확성'을 완전하고 모호하지 않게 명세하기란 매우 어렵다. 연구진은 대신 구글의 OSS-Fuzz 프로젝트에 이미 존재하는 퍼즈 테스트를 명세로 자동 변환했다. 퍼즈 테스트는 개발자가 지정한 진입점에 무작위에 가까운 입력을 대량으로 쏟아부어 크래시를 유발하는 입력을 찾는 방식인데, 이를 "64MB 미만의 어떤 입력에서도 이 테스트는 크래시하지 않는다"는 규칙으로 바꿔 RISC-V로 컴파일된 기계어 명령 위에 정의한 것이다. 이 명세를 증명해내면 해당 진입점에 대한 퍼징은 더 이상 버그를 찾을 수 없다는 의미가 된다.
클로드는 몇 주에 걸쳐 123개 OSS-Fuzz 라이브러리의 239개 진입점에서, 64MB 이하 모든 입력에 대해 크래시가 없음을 증명했다. 증명문은 Rocq 언어로 약 1억 8천만 줄에 달하며, 전형적인 증명 하나가 약 60만 줄, 대상 바이너리의 명령 수는 중앙값 기준 1만 8천 개 수준이었다. 중요한 전제가 붙는다. 단일 스레드 정적 바이너리, 고정된 메모리 예산, RISC-V CPU, 리눅스 OS 환경이라는 가정이다. 아키텍처와 OS 처리 모델을 표준화해 범위를 넓히는 일은 충분히 손닿는 과제라고 연구진은 본다.
신뢰해야 할 것은 증명문이 아니다
1억 8천만 줄이라는 규모에 압도될 필요는 없다. 사람이 그 방대한 증명문을 일일이 검토할 필요가 없기 때문이다. Rocq 증명 검사기가 명세가 실제로 충족됐는지 기계적으로 확인하므로, 개발자가 믿어야 할 대상은 Rocq 검사기와 RISC-V·리눅스 의미론 같은 소수의 '신뢰 기반' 요소뿐이다. 물론 이 요소들을 강화하는 일 자체가 가볍지는 않다. 그러나 수많은 코드를 일일이 디버깅하는 것보다는 훨씬 다루기 쉽고, 이 신뢰 기반의 크기를 키우지 않고도 임의로 많은 프로젝트를 보호할 수 있다는 점에서 확장성이 있다.
증명에 성공했다고 해서 그 라이브러리에 버그가 전혀 없다는 뜻은 아니라는 점은 분명히 짚어야 한다. 남은 버그는 신뢰 기반 요소 안에 있거나, 애초에 이 증명의 범위 밖에 있을 뿐이다. 그럼에도 과정 자체가 뜻밖의 소득을 냈다. 증명을 시도하는 동안 클로드가 수년간 발견되지 않았던 실제 버그 수백 개를 찾아낸 것이다. 퍼저가 사실상 건드리기 어려운 종류의 버그들이었다. 한 압축 해제 코드에서는 약 20MB 크기의 드문 특정 배치에서만 드러나는 카운터 언더플로가 범위 밖 쓰기로 이어졌고, 어떤 이미지 디코더에서는 64MB 입력과 2GB 넘는 메모리가 필요한 범위 밖 읽기가 나왔다. 같은 파일에 대한 두 핸들을 특정 순서로 호출해야만 발생하는 버그, libexpat의 CVE-2026-56132 재발견, 그리고 아예 크래시를 일으키지 않는 논리 버그(파일 접근 제한 기능이 항상 적용되지 않는 문제)까지 포착됐다.
실무자에게 남는 의미와 한계
한국의 개발 현장 관점에서 이 결과는 두 갈래로 읽힌다. 하나는 정형 검증이 더 이상 특정 산업의 전유물이 아니라, LLM을 활용하면 일반 오픈소스에도 적용을 시도해볼 만한 영역으로 내려왔다는 신호다. Theorem은 같은 파이프라인을 다른 오픈소스 프로젝트에 돌려주겠다고 밝혔고, 자체 코드 검증을 돕는 클로드 스킬도 공개했다. 다른 하나는 설령 완전한 증명에 이르지 못하더라도, 증명을 시도하는 과정 자체가 수조 번의 테스트로도 못 잡던 버그를 끌어낸다는 점이다. 즉 '증명 성공'이라는 최종 목표와 별개로 버그 발굴 수단으로서의 가치가 있다.
다만 전제 조건을 잊지 말아야 한다. 이번 증명은 단일 스레드, RISC-V, 리눅스라는 모델에 한정되며, 멀티스레드나 다른 아키텍처·OS는 아직 표준화 과제로 남아 있다. 명세를 자동으로 얻어낸 것도 이미 잘 정의된 퍼즈 테스트가 존재했기 때문이지, 브라우저처럼 '정확성'을 정의하기 어려운 소프트웨어 전반에 곧바로 통하는 방식은 아니다. 그럼에도 모델이 똑똑해질수록 증명 비용은 떨어지고, 코드가 형식화될수록 증명을 재사용·수정하며 비용을 분산할 수 있다는 방향성은 설득력이 있다. 과거에 덜 유능한 모델로 정형 검증을 시도했다가 포기한 팀이라면, 지금 다시 들여다볼 이유가 생긴 셈이다.