Anthropic 프런티어 레드팀은 10월 22일 연구 결과를 공개했다. Claude를 이용해 오픈소스 라이브러리 123개의 진입점 239개에 대한 형식 증명을 작성했으며, 입력이 64MB보다 작으면 이 프로그램들은 중단되지 않는다는 내용이다. 증명은 컴파일된 RISC-V 실행 파일 위에서 직접 이뤄졌고, 형식 도구를 만드는 Theorem이 협력사로 참여했다. Anthropic은 AI가 실서비스 소프트웨어의 어셈블리 수준에서 대규모 형식 검증을 한 것은 처음이라고 밝혔다.
대상 라이브러리는 모두 구글의 OSS-Fuzz 프로젝트에서 나왔다. 퍼징 플랫폼에 오랫동안 올라 있던 기반 컴포넌트들로, 압축, 이미지 디코딩, HTTP 파싱이 모두 포함돼 있다. 전체 작업에는 몇 주가 걸렸다.
퍼징 테스트를 정리로 바꾸다
방식은 세 단계다. 먼저 팀은 각 라이브러리가 이미 갖고 있던 퍼즈 테스트 모음을 "이 테스트 코드는 어떤 입력에도 중단되지 않는다"는 형식 명세로 다시 썼다. 명세는 Theorem이 제공하는 RISC-V 명령어 의미론과 Linux 프로세스 의미론 모델 위에 세워졌다.
두 번째로 Claude가 증명을 쓰고, Rocq 증명 검사기가 한 줄씩 대조한다.
"Claude writes the proof; the Rocq kernel checks it against the specification."
(Claude가 증명을 쓰면, Rocq 커널이 그것을 명세와 대조해 검사한다.)
세 번째 단계는 증명이 막히는 경우를 다룬다. 증명이 막히는 것은 코드에 실제로 결함이 있다는 신호인 경우가 많다. 이때는 Claude가 직접 코드를 고치고, 명세를 다시 생성한 뒤 증명을 이어 간다. 팀은 이 단계에서 모델이 증명을 통과시키려고 프로그램을 멋대로 바꾸는 "보상 해킹"이 생기기 쉽다고 인정했다. 그래서 패치에 페널티를 붙이고, 패치가 영향을 주는 입력 범위를 증명하도록 요구했으며, 모든 패치를 기록해 사람이 감사하게 했다.
전형적인 증명은 약 60만 줄이다. 결국 신뢰해야 하는 부분은 RISC-V와 Linux의 의미론 모델, 정리 진술 자체, 그리고 Rocq 검사기만 남는다.
증명 과정에서 찾아낸 취약점
증명 도중 발견되어 수정된 버그는 수백 건이며, 그중 일부는 퍼징으로 우연히 맞닥뜨리기 어렵다. 글에는 몇 가지 사례가 나온다. 압축 해제기의 카운터 언더플로는 약 20MB의 특정 입력에서만 발생한다. 이미지 디코더의 범위 밖 읽기는 64MB 입력에 2GB 이상의 메모리가 있어야 나타난다. 또 다른 범위 밖 읽기는 핸들 두 개가 같은 파일을 특정 순서로 조작해야 한다. libexpat의 CVE-2026-56132도 다시 발견됐다.
cpp-httplib 증명에는 또 하나의 고비가 있었다. std::set이 소멸될 때의 재귀가 스택 오버플로를 일으킬 수 있었던 것이다. 이를 배제하기 위해 팀은 libc++ 레드-블랙 트리의 균형 알고리즘이 트리 깊이를 로그 수준으로 억제함을 기계어 수준에서 증명했다.
같은 연구에는 몇 가지 곁가지 실험도 붙어 있다. Claude는 Rust로 Python 부분집합을 작성하고 Verus로 CPython 의미론에 부합함을 증명했으며, 무작위 프로그램 170만 개에서 CPython과 동작이 일치한 비율은 99.95%였다. 또 x86 명령어 의미론을 스스로 생성했는데, 한 단계씩 실행해 Ubuntu 사용자 공간을 부팅할 수 있었고, 그 과정에서 공식 참조 문서의 오류를 수백 건 찾아냈다.
seL4와 나란히 놓고 보면
형식 검증은 산업계에서 새로운 것이 아니며, 어려움은 늘 인력에 있었다. 업계에서는 seL4 마이크로커널을 자주 예로 든다. C 코드 약 1만 줄에 당시 증명 투입은 보통 20인년 안팎으로 인용된다. CompCert 컴파일러도 비슷한 길을 걸었으며, 작은 팀이 여러 해 동안 다듬었다. 이런 프로젝트의 공통점은 대상이 적고, 기간이 길고, 전문가가 많이 필요하다는 것이다.
이번 Anthropic의 규모는 라이브러리 123개를 몇 주에 처리한 것이다. 대략 견주어 보면 작업 단위당 비용 구조가 다른 모양으로 바뀌었고, 사람은 증명을 쓰는 자리에서 물러나 명세를 정하고 패치를 검토하는 쪽으로 옮겨 갔다. 대신 비용은 토큰으로 바뀌었다. 글에 따르면 완전한 증명 하나에 수억 토큰이 들 수 있다. 소형 과제 36개에서는 과제마다 에이전트 하나에게 세 번의 시도를 주고, 시도당 토큰 예산은 500만 개였다. 에이전트끼리 서로의 증명을 재사용하도록 허용하자 필요한 토큰이 17% 더 줄었다.
보증의 강도도 같은 수준이 아니다. seL4가 증명한 것은 기능적 정확성이지만, 이번에 증명한 것은 "중단되지 않는다"는 것뿐이어서 범위가 훨씬 좁다.
증명 바깥의 빈틈
Anthropic이 직접 꼽은 한계는 꽤 구체적이다. 증명은 싱글 스레드, 정적 링크, musl libc를 쓰는 RISC-V 바이너리를 기반으로 하지만, 대부분의 사용자가 실제로 돌리는 것은 x86이나 ARM에서 glibc를 동적 링크한 빌드다. AddressSanitizer 자체가 모든 메모리 안전성 오류를 잡아내지는 못하고, 다루지 못한 진입점도 있으며, 호출자가 라이브러리를 잘못 써서 생기는 메모리 손상도 증명 범위 밖이다.
"Formally verified" does not mean "bug-free."
("형식 검증됨"이 "버그 없음"을 뜻하지는 않는다.)
명세와 실제 기계 사이의 차이는 이 접근법에서 가장 문제가 생기기 쉬운 지점이다. Rocq와 여러 의미론 모델 자체도 보강이 필요하며, 글은 이를 "작은 일이 아니다"라고 표현했다. 팀의 판단은 형식 검증이 안전한 소프트웨어 개발의 일상적인 단계가 되리라는 것이다. 다만 이런 증명이 x86과 glibc 같은 주류 배포 환경까지 언제 확대될지는 글에 시점이 나와 있지 않다.
참고 출처: Anthropic 프런티어 레드팀 연구 글, CocoLoop, Anthropic 연구 페이지(라이브러리 수, 진입점 수, 증명 줄 수, 토큰 비교 기준을 확인).