Anthropic, Claude로 라이브러리 123개 진입점 239개에서 무충돌 증명

Anthropic이 협력사 Theorem과 함께 Claude로 오픈소스 라이브러리 123개의 보안 속성을 어셈블리 코드 수준(RISC-V)에서 증명했다고 2026년 10월 22일 발표했다. 형식 검증은 코드가 정해진 규칙을 항상 지킨다는 사실을 수학적으로 증명하는 기법인데, 지금까지는 전문가가 수년간 매달려야 해서 대부분의 실제 프로젝트에는 쓰기 어려웠다. Anthropic은 대규모 언어 모델이 이 증명을 대규모로 만들 수 있게 됐다고 밝혔다.

Anthropic은 증명 일부를 누구나 검증하고 재사용할 수 있도록 RISC-V와 운영체제 의미 모델(semantics)과 함께 공개했다. Theorem은 다른 오픈소스 프로젝트에도 같은 파이프라인을 돌려 주겠다고 제안했고, 개발자가 자기 코드를 검증해 볼 수 있도록 Claude 스킬도 내놓는다.

퍼징 테스트를 증명 대상으로 바꾼 방식

소프트웨어가 올바르다고 증명하려면 먼저 '올바름'이 무엇인지 명세(spec)로 적어야 한다. PNG 디코더처럼 명세가 분명한 프로그램도 있지만 텍스트 편집기나 웹 브라우저는 그렇지 않다. Anthropic은 이 문제를 피하려고 오픈소스 라이브러리에 이미 있는 퍼징 테스트를 명세로 자동 변환했다. 퍼징은 개발자가 만든 진입점에 무작위로 변형한 입력을 엄청나게 쏟아부어 충돌을 찾는 방식인데, 입력이 무한해서 모든 경로를 훑었다고 보장하지 못한다.

변환한 명세는 '64MB 미만의 어떤 입력에도 이 퍼징 테스트가 충돌하지 않는다'는 내용이다. Claude가 이를 증명하면 RISC-V 환경에서 그 진입점을 퍼징해도 더는 버그가 나오지 않는다. 대상은 Google의 OSS-Fuzz 프로젝트에 속한 라이브러리이며, OSS-Fuzz는 C와 C++ 프로그램에 AddressSanitizer(ASan)를 자동으로 붙여 메모리를 잘못 접근하면 곧바로 충돌하게 한다.

컴파일한 RISC-V 실행 파일과 Theorem의 RISC-V·Linux 프로세스 의미 모델, 원하는 무충돌 속성이 합쳐져 증명이 만족해야 할 명세가 기계적으로 만들어진다. Claude가 증명을 쓰면 Rocq 증명 검사기가 명세를 만족하는지 확인한다.

증명 규모와 발견한 버그

Claude는 몇 주에 걸쳐 발견한 버그를 직접 패치한 뒤, OSS-Fuzz 라이브러리 123개의 진입점 239개에서 64MB 이하 어떤 입력에도 충돌하지 않음을 증명했다. 증명은 Rocq 코드 약 1억 8,000만 줄이고, 증명 하나는 보통 약 60만 줄이다. 대상 바이너리의 중간 길이는 RISC-V 명령어 1만 8,000개다.

코드량은 방대하지만 사람이 검토할 필요는 거의 없다. 개발자가 믿어야 할 대상은 RISC-V와 Linux 프로세스의 형식 모델, 증명된 정리의 정확한 문장, Rocq 증명 검사기 세 가지다. 따라서 이 라이브러리에 버그가 없다는 뜻은 아니다. 남은 버그는 이 세 가지 안에 있거나 증명 범위 밖에 있다는 의미다. 이 방식은 신뢰해야 할 구성요소를 늘리지 않고도 프로젝트를 계속 보호할 수 있다고 Anthropic은 설명했다.

증명을 시도하는 과정에서 수백 개의 버그가 나왔다. 사람이 매번 개입하지 않도록 Claude가 직접 코드를 패치하면 명세가 다시 만들어지고, Claude는 새 명세를 증명했다. 증명을 쉽게 하려고 프로그램을 항상 충돌하지 않는 것으로 바꿔 버리는 보상 해킹을 막기 위해 패치에는 감점을 주고, 바뀌는 입력이 적다는 것을 증명하면 가산점을 줬다. 패치는 기록해 감사도 했다.

퍼저가 찾기 어려운 버그가 많았다. 퍼저는 보통 1MB 이하의 작은 입력을 변형하고 코드 커버리지로 방향을 잡는다. 한 라이브러리에서는 압축 해제기의 카운터 언더플로가 범위 밖 쓰기로 이어졌는데, 특이한 구조를 가진 약 20MB 입력에서만 발생했다. 이미지 디코더에서는 64MB 입력과 2GB 넘는 메모리가 있어야 나오는 범위 밖 읽기가, 다른 라이브러리에서는 같은 파일의 핸들 두 개에 특정 순서로 호출해야 나오는 범위 밖 읽기가 발견됐다. libexpat의 CVE-2026-56132도 깊게 중첩된 입력으로 다시 찾아냈다. 충돌하지 않는 논리 버그도 있었다. 한 라이브러리에서는 애플리케이션이 불러올 수 있는 파일을 제한하는 기능이 항상 적용되지는 않았다.

퍼징 테스트는 인코딩 후 디코딩하면 원래대로 돌아오는지 같은 상위 속성을 검사하는 경우가 많다. LZO 압축 알고리즘의 퍼징 테스트는 압축한 뒤 풀면 원본과 같다고 단언하므로, 충돌하지 않음을 증명하면 그 속성을 증명한 것과 같다. cpp-httplib 증명에서는 std::set 소멸자의 재귀로 스택 오버플로가 나지 않음을 보여야 했고, 그러려면 libc++ 레드블랙 트리 재균형 알고리즘이 트리 깊이를 로그 수준으로 유지한다는 것을 기계어 수준에서 증명해야 했다.

다른 형식 검증 사례

주요 제약 하나는 비용이다. 증명 하나를 만드는 데 수억 토큰이 들 수 있다고 Anthropic은 밝혔다. OSS-Fuzz 코드로 작은 검증 과제 36개를 만들어 비교하니 Opus 5.5는 그중 절반을 Opus 5보다 약 40% 적은 토큰으로 증명했다. 증명을 서로 복사할 수 있는 공유 작업공간에서는 에이전트가 혼자 할 때보다 토큰을 17% 적게 썼고, 혼자서는 실패했다가 성공한 경우도 있었다. 완료된 증명 34개 중 30개에서 혼자 작업한 평균 비용이 더 높았고, 혼자서는 두 개를 끝내지 못했다. 실제 작업에서도 C 런타임과 ASan 초기화 부분의 증명이 프로그램끼리 많이 겹쳐, 팀들이 다른 팀의 증명을 복사해 고쳐 썼다.

비용과 한계

가장 큰 제약은 비용이다. 증명 하나를 만드는 데 수억 토큰이 들 수 있다고 Anthropic은 밝혔다. OSS-Fuzz 코드로 작은 검증 과제 36개를 만들어 비교하니 Opus 5.5는 그중 절반을 Opus 5보다 약 40% 적은 토큰으로 증명했다. 증명을 서로 복사할 수 있는 공유 작업공간에서는 에이전트가 혼자 할 때보다 토큰을 17% 적게 썼고, 혼자서는 실패했다가 성공한 경우도 있었다. 완료된 증명 34개 중 30개에서 혼자 작업한 평균 비용이 더 높았고, 혼자서는 두 개를 끝내지 못했다. 실제 작업에서도 C 런타임과 ASan 초기화 부분의 증명이 프로그램끼리 많이 겹쳐, 팀들이 다른 팀의 증명을 복사해 고쳐 썼다.

바이너리 수준에서 일반적인 명세로 작업하면 코드베이스를 다른 언어로 다시 쓰지 않아도 된다. 패키지 단위로 증명을 재사용할 수 있어 의존성 하나는 한 번만 검증하면 된다. Theorem은 glibc, OpenSSL, cURL 같은 핵심 인프라를 포함한 Nix 생태계 전체를 검증하는 로드맵을 내놓았다.

'형식 검증됨'은 '버그 없음'이 아니라고 Anthropic은 강조했다. 첫째 한계는 실제 기계와 모델의 차이다. 증명은 musl libc에 링크한 단일 스레드 정적 RISC-V 바이너리를 다루지만, 대부분의 사용자는 x86이나 ARM에서 glibc에 동적으로 링크해 쓴다. 이를 메우려면 x86 의미 모델 등 실제 배포 환경에 가까운 시스템 모델이 필요하다. 둘째는 증명 범위다. ASan은 모든 메모리 안전성 버그를 잡지 못하고, 라이브러리마다 모든 진입점을 검증한 것도 아니며, 모든 진입점을 검증해도 죽은 코드 등으로 라이브러리 전체가 덮이지는 않는다. 호출하는 쪽이 라이브러리를 잘못 쓰면 호출자 쪽 메모리가 손상될 수도 있다.

Anthropic은 모델이 좋아질수록 증명 작성 비용이 떨어지고, 증명이 표준화되어 코드베이스 사이에서 재사용될수록 비용이 분산될 것으로 내다봤다. 과거에 성능이 낮은 모델로 형식 검증을 시도해 실패한 개발자도 다시 해 보라고 권했다. 형식 검증이 앞으로 지금의 퍼징만큼 흔한 도구가 될 것이라는 전망도 내놓았다.