Anthropic Claude 형식 검증: 라이브러리 123개 크래시 부재 증명

핵심 요약

Anthropic은 공식 연구 페이지에서 Theorem과의 협업 결과를 공개했다. Claude(Opus 5.5)가 OSS-Fuzz의 오픈소스 라이브러리 123개, 진입점 239개를 대상으로 "64MB 미만의 어떤 입력에서도 크래시가 없다"는 성질을 증명했다(Anthropic 공식). 증명은 Rocq 증명 검사기가 기계적으로 검사한다.

무엇을 증명했나

이 증명은 전제 위에서 성립한다. 대상은 단일 스레드 정적 바이너리다. 메모리 예산은 고정이다. CPU는 RISC-V, OS는 Linux 모델이고 libc는 musl을 정적 링크한다(Anthropic 공식).

즉 소스 코드가 아니라 컴파일된 바이너리의 명령어 수준에서 성질을 증명한다. 대상 바이너리 길이의 중앙값은 RISC-V 명령어 18,000개다(Anthropic 공식).

규모와 방법

1. 증명 분량

총 Rocq 증명은 약 1.8억 줄이다. 전형적인 증명 1건은 약 60만 줄이다(Anthropic 공식).

2. 검증 도구

기본 검증기는 Rocq 증명 검사기다. Python 인터프리터 관련 작업에는 Verus를 사용했다(Anthropic 공식). 협업사 Theorem은 다른 프로젝트 검증에 쓸 수 있는 Claude 스킬도 공개했다.

3. 비용 지표

OSS-Fuzz 코드 기반의 소규모 검증 과제 36건에서 Opus 5.5는 절반을 증명하는 데 Opus 5보다 약 40% 적은 토큰을 썼다. 여러 에이전트가 증명을 공유 작업공간에서 재사용하면 토큰이 17% 줄었다(Anthropic 공식).

4. 버그 발견

증명 과정에서 수백 개의 버그가 발견됐다. 정확한 개수는 공개되지 않았다(Anthropic 공식). ExplainX는 libexpat의 CVE-2026-56132가 재발견됐다고 전했다(2차 보도). 이 내용은 공식 페이지에서 확인하지 못했다.

공개 범위

실무 적용 시사점

퍼징은 입력을 던져 크래시를 찾는 방식이다. 이 연구는 "찾지 못했다"가 아니라 "전제 안에서 존재하지 않는다"를 검사기로 확인한다. 라이브러리 유지보수자는 공개된 명세와 Theorem의 Claude 스킬을 자기 프로젝트 검증에 시험해 볼 수 있다.

다만 환경 차이를 봐야 한다. 증명은 RISC-V와 musl 가정에서 성립한다. 대부분의 사용자는 x86이나 ARM에서 동적 링크된 glibc를 쓴다(Anthropic 공식). 증명 결과를 그대로 자기 배포 환경에 적용할 수 없다.

공식 명시 한계

• "형식 검증됨"은 "버그 없음"이 아니다. 명세가 실제 기계와 일치해야 한다.
• AddressSanitizer는 모든 메모리 안전 버그를 잡지 못한다.
• 모든 진입점이 검증된 것은 아니며 데드코드는 다루지 않는다.
• 실제 호출자가 라이브러리를 오용해 메모리를 손상시킬 수 있다.
• 신뢰 기반이 남는다. Rocq 검사기, 하드웨어, OS, OCaml 컴파일러다.
• 보상 해킹 위험이 있다. 프로그램을 사소하게 고쳐 정리를 증명 가능하게 만들 수 있어, 패치는 감점하고 감사한다.

장단점

장점은 기계 검사가 가능한 증명, 명시된 전제, 증명 일부와 의미론의 공개다. 한계는 RISC-V·musl 가정, 진입점 일부만 검증된 범위, 신뢰 기반 잔존, 보상 해킹 위험이다.

전망

공식 페이지의 비용 지표는 두 가지다. 모델이 Opus 5에서 Opus 5.5로 바뀌며 토큰 사용이 줄었고, 증명 재사용으로 17%가 더 줄었다. 다만 검증 대상 확대 범위와 일정, 다른 아키텍처(x86/ARM)와 glibc 지원 계획은 공식 페이지에서 확인되지 않았다. 증명 일부와 명세는 GitHub에 공개되어 있어 외부 연구자가 직접 검토할 수 있다.

결론

이 연구는 LLM이 대규모 형식 증명을 생성하고 검사기가 이를 통과시킨 사례다. 공식 페이지가 한계를 구체적으로 적은 점은 평가할 만하다. 보안 엔지니어, C/C++ 라이브러리 유지보수자, 형식 검증 연구자가 읽어볼 가치가 있다. 다만 증명의 전제가 RISC-V와 musl로 한정되므로 일반 배포 환경의 안전을 그대로 보증하지는 않는다. 평점은 4점이다.