Anthropic, Theorem과 Claude 기반 123개 오픈소스 라이브러리 형식 검증 성공

• Anthropic과 Theorem이 LLM(Claude)을 활용해 대규모 형식 검증이 가능함을 입증함. RISC-V 어셈블리 레벨에서 123개의 오픈소스 라이브러리(239개 엔트리 포인트)의 보안 속성을 증명함
• 64MB 이하의 모든 입력을 검증 대상으로 삼아, 모델링된 Linux OS 응답 하에서 메모리 안전성 오류나 애서션 실패 없이 프로그램이 정상 종료됨을 증명함
• 약 1억 8,000만 줄의 Rocq 증명 코드를 생성함. 증명당 평균 60만 줄, 바이너리당 중앙값 18,000개의 RISC-V 명령어 사용
• Fuzzer가 놓친 버그를 Claude가 식별하고 패치함. 압축기 카운터 언더플로우, 이미지 디코더의 범위 밖 읽기, 파일 로딩 제한 로직 버그 포함

Methodology and Efficiency

• 기존 퍼즈 테스트를 테스트 스위트가 항상 통과한다는 규칙으로 변환하여 RISC-V 컴파일 바이너리의 명세로 활용함
• Opus 5.5가 36개 검증 작업의 절반을 완료했으며, Opus 5보다 약 40% 적은 토큰을 사용함
• 에이전트가 워크스페이스를 공유하고 증명을 복사하도록 허용했을 때 독립 작업 대비 토큰 사용량이 17% 감소함. 완료된 34개 증명 중 30개가 단독 작업 평균 비용보다 적은 토큰을 사용함

Case Studies and Results

• Rust 기반 Python 인터프리터가 Verus를 통해 CPython 시맨틱을 따름을 증명함. 170만 개의 랜덤 테스트 프로그램 중 99.95%에서 CPython 동작과 일치함
• 널리 사용되는 PDF 리더 검증에서 1년치 보고서에 해당하는 보안 버그를 1주 만에 발견함. 10년 이상 잠재된 로직 버그 포함
• x86 ISA 형식 시맨틱을 사용해 Linux 커널의 zlib 구현이 RFC 1950에 정확함을 증명하고, 경미한 버그를 발견함

Limitations and Scope

• 현재 증명은 musl libc와 링크된 단일 스레드, 정적 RISC-V 바이너리로 제한됨. 프로덕션 환경은 주로 동적 glibc 링크를 사용하는 x86/ARM 아키텍처임
• '형식 검증 완료'는 버그가 없는 소프트웨어를 보장하지 않음. 증명 체크어는 명세가 실제 하드웨어나 OS 동작과 일치하는지 검증할 수 없음
• 모든 엔트리 포인트나 데드 코드를 커버하지 않으며, 잘못된 호출자 사용으로 인한 메모리 손상 위험은 여전히 존재함