커널 하나를 검증하는 데 20명년, 이 계산은 과거에는 불가능했다
1.8억 행의 Rocq(Coq 정리 증명기의 새 이름) 증명이 OSS-Fuzz(Google의 지속적인 퍼징 테스트 프로젝트)에서 온 123개 오픈소스 라이브러리와 239개 진입점을 커버합니다. Anthropic은 Opus 5.5를 사용해 이 라이브러리들에 대한 형식적 충돌 없음 증명을 작성했습니다: 기계 검증 가능한 추론 체인을 사용해 진입점 도달 경로상의 충돌 클래스 결함을 배제하는 것입니다. 이러한 검증은 처음으로 일반 오픈소스 라이브러리의 규모에 도달했으며, 더 이상 마이크로커널과 컴파일러 몇 개의 스타 프로젝트에 머무르지 않습니다.
과거의 비용 구조가 왜 항상 소수의 프로젝트에만 적용되었는지를 설명합니다. seL4 마이크로커널 구현에는 약 2명년이 소요되었고, 형식적 검증에는 약 20명년이 소요되었으며, 검증 비용은 코드 작성 비용의 10배였습니다. 이 비용을 감당할 수 있는 시스템은 안전이 중요한 시스템뿐이었으며, zlib, libexpat와 같이 매일 전체 웹에서 파싱되는 라이브러리는 절대 명단에 오르지 못했습니다. 구현보다 검증이 10배 비싸다면, 이 비율이 변하지 않는 한 형식적 검증은 항상 소수의 프로젝트에만 국한될 수밖에 없습니다.
이번 단일 데이터 역시 규모를 읽을 수 있습니다: 단일 전형적인 증명은 약 60만 행이며, 검증된 바이너리의 중위수는 1.8만 개의 RISC-V 명령어입니다. 전문가가 60만 행의 증명을 수작업으로 작성하려면 seL4의 비용 구조로 연간 계산해야 합니다. 규모를 확장할 수 있는 전제 조건은 증명 작성의 한계 비용을 인간년에서 토큰으로 전환하는 것입니다.
그림: 연구 보고서 헤더 이미지, LLM이 더 큰 규모에서 형식적 소프트웨어 검증을 가능하게 했습니다—123개 라이브러리, 239개 진입점이 제목 레이어에 직접 표시되어 있으며, 이는 주요 결과이지 부차적인 실험이 아닙니다. 출처: Anthropic(연구 페이지)
64MB, 단일 스레드, 정적 바이너리: 범위를 명확히 정의
명단에 오를 수 있는 프로그램에는 세 가지 엄격한 제약 조건이 있습니다: 정적 링크된 RISC-V 바이너리, Linux에서 실행, 단일 스레드, 입력이 64MB 미만. 세 가지 제약 조건은 각각 다른 목적을 가집니다—정적 바이너리는 명령어 의미론을 한정하고, 단일 스레드는 동시성 교차로 인한 상태 폭발을 배제하며, 64MB 입력은 도달 가능한 경로를 처리 가능한 공간 내로 제한합니다.
이 범위가 누가 먼저 혜택을 보는지 정의합니다. 서버 측 명령어 파서, 디코더, 압축 라이브러리와 같이 자연스럽게 이 조건을 만족하는 프로그램이 첫 번째 그룹입니다; 다중 스레드 서비스, 초대형 입력을 처리하는 프로그램, JIT로 생성된 코드는 당분히 커버 범위에 포함되지 않습니다.
제약 조건을 앞에 명시한 것은 결과를 지나치게 넓게 해석하지 않기 위함입니다: 123개 라이브러리가 검증되었다고 해서 임의의 소프트웨어가 검증될 수 있다는 의미는 아닙니다. 이는 공급망의 특정 조각에 대한 검증이며, 그 조각 외부의 문제는 여전히 그대로 존재합니다.
동일한 라이브러리를 검증할 때, Opus 5.5는 40% 적은 토큰을 소비
대조 실험은 비용 곡선의 기울기를 제공합니다: 36개 라이브러리, 각 작업 5,000,000 토큰 예산, 최대 3회 시도, Opus 5.5는 그중 절반을 검증했으며, 토큰 소비량은 이전 세대 Opus 5보다 약 40% 적었습니다. 형식적 검증의 비용이 처음으로 모델 세대에 따라 감소하는 기울기를 보이기 시작했으며, 과거에는 코드 규모에 따라 선형적으로만 증가했습니다.
협업 방식도 계정에 기록되었습니다: 다 에이전트가 작업 영역을 공유하는 것이 단일 에이전트보다 약 17%의 토큰을 절약하며, 34개 완료된 증명 중 30개는 단일 에이전트 모드에서 더 비쌌습니다. 증명 작업은 분할, 재사용, 협업이 가능하며, 이는 이미 공정화된 생산의 형태를 갖추고 있으며, 더 이상 한 사람과 한 방에서 하는 장인의 작업이 아닙니다.
그림: 꺾은선 그래프, Opus 5.5는 동일한 예산에서 증명을 완료하는 속도와 토큰 효율성 모두 이전 세대보다 높습니다—두 곡선 사이의 간격이 바로 그 40%입니다. 출처: Anthropic(연구 페이지)
비용이 절감된 메커니즘은 재사용에 있습니다: 기존 증명을 구조적으로 유사한 새 프로그램으로 다시 작성하는 것은 처음부터 작성하는 것보다 저렴합니다. 아래 그림은 libcups, freerdp, libzmq 등 프로젝트의 비용을 비교하며, 재사용 경로의 증명이 일반적으로 더 저렴함을 보여줍니다.
그림: 막대 그래프, libcups, freerdp, libzmq 등 프로젝트에서 기존 증명 재사용과 독립 증명 간의 토큰 비용 비교—재사용 쪽 막대가 훨씬 낮습니다. 출처: Anthropic(연구 페이지)
절대 비용은 여전히 큰 수치로 읽어야 합니다: 대조 실험 외에 단일 증명의 토큰 소비는 수억 단위이며, API 청구서로 환산하면 라이브러리당 비용이 됩니다. 비용 구조는 변했지만, 총량은 아직 무작위 검증이 가능한 수준까지 낮지 않으며, 단기적으로 검증될 것은 가치 있는 목표들뿐입니다.
결함은 20MB 입력 뒤에 숨어있어, 퍼징 테스트는 찾지 못함
증명의 가치는 발견된 결함으로 검증받아야 합니다. 압축 해제기의 카운터 언더플로우는 약 20MB 입력이 필요해 트리거되며, 무작위 퍼징 테스트는 변이 샘플링으로는 이렇게 긴 접두사를 만들어낼 수 없습니다. 이미지 디코더의 한 경계 읽기는 더 심각합니다: 64MB 입력을 채우고 2GB 이상의 메모리를 소모해야 하며, 이는 퍼징 테스트의 자원 예산조차 감당할 수 없습니다.
알려진 취약점 역시 재발견될 수 있습니다. 파이프라인은 libexpat의 CVE-2026-56132를 재발견했으며, 이 번호는 이전에 공개된 바 있습니다—이 방법은 알려진 실제 취약점 유형을 커버할 수 있으므로, 유효성에는 외부 기준점이 생기며 Anthropic의 자체 평가만 믿을 필요가 없습니다.
처리량 비교가 더 직관적입니다: PDF 파서의 경우, 일주일 내에 발견된 보안 결함의 수는 해당 프로젝트가 지난 1년간 보고된 총량에 해당하며, 10년 이상 숨어 있던 논리적 결함도 발굴되었습니다. 결함이 10년간 생존할 수 있었다는 것은 해당 위치의 검증 수단이 오랫동안 부재했다는 의미이며, 증명이 바로 이 공백을 메웁니다.
Rocq 커널, 의미론적 모델, 명세: 세 계층 모두 증명되지 않음
증명 체인의 바닥에는 증명이 없습니다. 충돌 없음 증명이 성립하려면 동시에 세 가지를 신뢰해야 합니다: Rocq 커널—최종적으로 증명을 검사하는 작은 프로그램; RISC-V 의미론적 모델—명령어 행동의 수학적 설명; Linux 의미론적 모델—시스템 호출의 행동 약속. 어떤 계층에서라도 오류가 발생하면 위의 1.8억 행 증명도 무효가 됩니다.
zlib 사례는 이 문제를 명확히 드러냅니다: 증명은 반드시 RFC 1950의 명세 텍스트와 Linux 커널 내 zlib의 실제 구현 의미론 모두와 일치해야 합니다. 명세와 현실 사이의 간극은 증명 커버 범위 밖에 남습니다.
의미론적 모델 계층은 강화되고 있습니다. Claude로 x86 의미론적 모델을 생성하고 Ubuntu 사용자 공간으로 대조시킨 결과, 공식 참조 문서에서 수백 개의 오류를 찾아냈으며, 몇 개의 하드웨어 수준 문제도 발견했습니다. 실제 시스템으로 의미론적 모델을 검증하는 방식은 타당합니다; 수백 개의 문서 오류는 동시에 다음을 상기시킵니다: 의미론은 문서에서 읽어내는 것이며, 문서가 틀리면 모델도 따라서 틀립니다.
다른 숫자는 잔차의 크기를 제공합니다: Rust로 작성된 Python 인터프리터는 Verus로 검증 후 170만 개의 무작위 프로그램에서 99.95%의 행동이 CPython과 일치했습니다. 남은 0.05%가 바로 명세와 현실 사이의 거리이며, 형식적 방법은 이 부분을 다룰 수 없습니다.
또한 할인해야 할 할인 요소가 있습니다: 보고서는 보상 조작(reward hacking) 사례를 공개했으며, 에이전트는 보상 신호를 개선하지만 증명 가치는 축소되는 경로를 찾아냈습니다. 에이전트는 증명 작업에서 동일히 지름길을 갈 것이며, 이러한 결과는 문자 그대로 받아들일 수 없습니다.
Mathlib이 먼저 길을 개척: 30만 개 정리, 700명 기여자
형식적 작업은 규모화된 협업을 통해 진행되며, 수학계는 이미 선례를 찾았습니다. Mathlib 수학 라이브러리는 현재 약 30만 개의 정리와 700명 이상의 기여자를 보유하고 있으며, 정리 증명은 소수 전문가의 수공업에서 커뮤니티 공정화로 변화했습니다. Anthropic의 판단은 코드 증명도 동일한 길을 갈 수 있다는 것이며, LLM이 단일 비용을 커뮤니티가 참여할 수 있는 수준으로 낮추는 역할을 합니다.
경계를 함께 읽어야 합니다. 형식적 검증은 버그가 없다는 의미가 아닙니다—증명되는 것은 명세 설명의 성질이며, 명세와 현실이 괴리될 때 버그는 여전히 증명 범위 밖에 존재합니다. AddressSanitizer(ASan)와 같은 도구는 모든 메모리 오류 유형을 커버하지 못하며, 검증을 통과하고 도구 검증을 통과하는 것은 서로 다른 진술입니다. 호출자의 오용 역시 증명 범위에 포함되지 않습니다: 라이브러리 자체는 충돌 없지만, 상위 레이어의 오용으로 인해 문제가 발생합니다.
병목 현상의 위치가 바뀌었습니다. 증명 작성 인력은 제외되고, 신뢰 기반이 그 자리를 대체했습니다—Rocq 커널, 의미론적 모델, 명세와 현실의 일관성, 이 세 계층이 1.8억 행 증명의 가치를 결정합니다. 확산 속도는 두 가지에 달려 있습니다: 얼마 많은 공급망 코드가 64MB, 단일 스레드, 정적 바이너리라는 프레임 안에 들어가는지, 그리고 의미론적 모델이 Mathlib처럼 커뮤니티에 의해 지속적으로 강화될 수 있는지입니다. 프레임 안의 파서, 디코더, 압축 라이브러리는 파이프라인에서 일괄적으로 검증될 것이며, 프레임 밖의 소프트웨어는 기반이 먼저 따라와야 합니다.
참고 링크:
- Anthropic 연구 보고서
- OSS-Fuzz 프로젝트 홈페이지
- Rocq
