1억 8천만 줄의 증명보다 중요한 것: Anthropic×Theorem 결과를 읽는 법

"AI가 123개 오픈소스 라이브러리를 형식 검증했다"는 문장은 읽는 순간 "그 라이브러리들은 이제 버그가 없다"로 미끄러지기 쉽습니다. 실제로 증명된 것은 훨씬 좁고, 그 좁음이 오히려 유용합니다. Anthropic과 Theorem이 공개한 결과는 239개 퍼징 진입점이 특정 실행 모델 아래에서 절대 크래시하지 않는다는 증명입니다. 1억 8천만 줄은 그 증명을 담은 Rocq 코드의 양이고, 의사결정에 필요한 숫자는 따로 있습니다.

10월 22일 발표를 적용하려면 “어떤 속성인가”와 “어떤 바이너리인가”를 함께 고정해야 합니다. 10월 26일 다시 읽은 Theorem의 범위 문서는 현재와 다음 툴체인의 종료 코드를 따로 설명합니다. 따라서 문서의 최신 상태를 오래된 증명에 그대로 적용해서도 안 됩니다. 이 글은 공개 증명 전체를 재검증하지 않았습니다.

증명된 것과 증명되지 않은 것

Anthropic의 연구 글과 Theorem의 what-gets-proven 문서를 대조하면 범위가 선명해집니다.

핵심은 "라이브러리 전체"가 아니라 "퍼징 진입점"입니다. 한 라이브러리에 여러 진입점이 있고, 그중 일부만 증명됐습니다. 진입점 밖의 코드, 호출자의 오용, 다른 아키텍처로 빌드한 바이너리는 이 명제의 범위 밖입니다.

왜 소스가 아니라 어셈블리인가

소스 수준 검증은 "소스가 맞다"를 증명합니다. 하지만 실제로 실행되는 것은 컴파일러와 링커를 거친 바이너리입니다. 컴파일러 최적화, 런타임 라이브러리, 링크 방식이 바뀌면 소스가 같아도 동작이 달라질 수 있습니다.

바이너리 수준 검증은 이 간극을 줄입니다. Theorem은 빌드를 두 번 수행해 바이트가 같은지 확인하고, 바이너리의 SHA-256을 lock에 고정합니다. 증명은 그 바이너리에 대한 것입니다. 재현 빌드가 전제이므로, 소스 커밋과 빌드 파일과 툴체인 이미지가 함께 공개됩니다.

대신 비용이 있습니다. 증명이 특정 아키텍처와 컴파일러에 묶입니다. x86-64로 빌드한 OSS-Fuzz 바이너리, 동적 링크된 glibc, 다른 최적화 플래그는 별개의 대상입니다. "이 라이브러리는 검증됐다"가 아니라 "이 커밋을 이 툴체인으로 빌드한 이 바이너리의 이 진입점은 검증됐다"가 정확한 문장입니다.

명세는 fuzz target 안에 있다

Theorem의 문서에서 가장 중요한 경고는 이것입니다. "증명은 fuzz target만큼만 강하다. 약한 fuzz target은 정리를 공허하게 만든다." 형식 검증에서 명세는 별도 문서가 아니라, 입력을 넣고 실패 조건을 검사하는 코드 자체입니다.

Theorem의 계약은 일반적인 fuzzer와 다릅니다. halts 명제는 종료 상태 0 또는 2만 받습니다. 0은 fuzz target이 정상 반환했다는 뜻이고, 2는 드라이버가 입력을 거부했다는 뜻입니다(예: 64MiB 이상). 그래서 예상된 오류는 return 0으로 끝내야 하고, 진짜 속성 위반은 abort()로 끝내야 합니다.

현재 증명에 고정된 드라이버에서 return -1은 실패가 아닙니다. 오히려 "이 입력은 코퍼스에 넣지 마라"는 신호로 해석되어 통과로 계산됩니다. assert()도 쓰면 안 됩니다. NDEBUG가 정의된 릴리스 빌드에서는 검사가 사라지기 때문입니다.

다음은 이해를 돕기 위한 가상의 decode API 예시입니다. 실제 컴파일이나 검증을 수행한 코드가 아닙니다.

// 잘못된 예: 속성 실패를 -1로 반환한다.
// halts 명제는 -1을 통과로 세므로, 속성이 깨져도 증명이 성립한다.
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  if (size < 4) return -1;
  if (!decode_is_valid(data, size)) return -1;
  return 0;
}

// 개선된 예: 예상된 오류는 0, 속성 위반은 abort().
// 단일 스레드, 입력 외 상태 없음, 입력 크기 상한을 지킨다.
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  if (size < 4) return 0;
  if (size >= 64u * 1024u * 1024u) return 0;

  struct decoded out = {0};
  if (!decode(data, size, &out)) return 0;   // 잘못된 입력은 정상적인 결과
  if (out.len > MAX_DECODED) abort();        // 명세 위반
  if (!roundtrip_matches(data, size, &out)) abort();
  free_decoded(&out);
  return 0;
}

여기서 abort()가 걸리는 조건이 곧 "이 라이브러리에서 절대 일어나면 안 되는 일"입니다. out.len > MAX_DECODED가 실제로는 허용되는 동작이라면, 증명은 틀린 명세를 완벽하게 증명하게 됩니다. 이 예제는 증명기와 별개로 명세 오류가 남을 수 있음을 보여줍니다.

명세의 공허함을 줄이기 위해 도입 전에 다음 두 가지를 점검할 것을 권합니다. 아래 항목은 이 글의 검토 기준이며 모든 공개 증명에 대해 확인한 결과가 아닙니다. 하나는 커버리지 증인입니다. 예제 입력들이 각 API 호출과 각 속성 검사를 최소 한 번씩 실행해야 합니다. 다른 하나는 구분 변이입니다. 속성을 일부러 한 줄 깨뜨렸을 때 fuzz target이 실제로 abort()하는 입력을 찾아야 합니다. 검사가 실제로 도달 가능한지 확인하지 않으면 “검사가 실행되지 않는 명세”를 증명할 수 있습니다.

빌드를 바꾸면 증명도 다시 연결해야 한다

검토 기록은 다음 네 칸으로 관리할 수 있습니다. 실제 프로젝트에서 실행한 검증 결과가 아니라 도입 문서의 작성 예시입니다.

현재 문서는 다음 툴체인에서 일부 언어 드라이버의 -1 반환을 상태 3으로 구분할 계획도 적습니다. 기존 증명은 고정된 드라이버를 유지합니다. 따라서 “항상 0과 2만 허용한다”는 문장을 모든 미래 빌드로 일반화하지 마세요. 또한 메모리 부족에 대한 임의 실패를 모두 견딘다는 보장은 별도 allocation-failure 타깃 없이는 얻지 못합니다.

첫 검증 대상은 어떻게 고르나

모든 코드를 한 번에 검증할 수는 없습니다. 다음 질문에 답하면서 후보를 좁히세요.

첫 대상으로는 작은 파서나 디코더가 적합합니다. 예를 들어 설정 형식 파서, 이미지 헤더 파서, 압축 해제 함수입니다. 반대로 플러그인 로더, 네트워크 서버, 멀티스레드 런타임은 현재 모델의 범위를 벗어납니다.

비용도 현실적으로 봐야 합니다. Theorem은 프로젝트당 고정된 기간을 약속하지 않고, 증명 하나에 며칠 이상 걸릴 수 있다고 밝힙니다. 빌드에는 Docker, buildx, Python 3, 약 10GB의 여유 공간이 필요하고, 첫 실행에서 약 1.1GB 툴체인 이미지를 내려받아 약 5GB로 풀립니다. tools/check는 네트워크 접근이 가능한 Dockerfile을 빌드하므로, 신뢰하는 저장소에서만 실행해야 합니다.

증명이 덮지 않는 것

도입 검토 문서에는 다음 한계를 명시하는 편이 좋습니다.

• 다른 빌드: 다른 컴파일러, 다른 플래그, 다른 아키텍처, OSS-Fuzz의 x86-64 빌드는 별개입니다.
• 다른 링크 방식: 증명은 정적 RISC-V 바이너리와 musl을 전제로 합니다. 대부분의 배포는 x86/ARM에서 glibc를 동적으로 링크합니다.
• 라이브러리 전체: 239개 진입점은 123개 라이브러리의 일부입니다. 진입점이 없는 코드, 죽은 코드, 호출자 쪽 메모리 오염은 범위 밖입니다.
• 탐지기의 공백: LeakSanitizer는 꺼져 있고, MemorySanitizer는 없습니다. 초기화되지 않은 메모리 읽기는 검사하지 않습니다.
• 큰 입력과 메모리: 64MiB 이상 입력, 메모리 예산을 넘는 입력은 명제에 포함되지 않습니다.
• 신뢰 기반: Rocq, RISC-V·Linux 의미론, 정리 문장 자체가 틀리면 원하는 보장과 어긋날 수 있습니다. 이 부분은 여전히 사람이 검토해야 합니다.
• 패치의 품질: 증명 과정에서 나온 수정은 AI가 만들었고, 사람이 검토했다는 보장이 없습니다. Theorem도 패치를 받은 뒤 검토하라고 명시합니다.

"형식 검증됐다"를 "버그 없음"으로 바꾸지 마세요. 정확한 문장은 "이 바이너리의 이 진입점은 이 명세를 만족한다"입니다.

1억 8천만 줄을 비용으로 읽기

줄 수는 규모를 보여주지만 비용을 말해주지 않습니다. 1억 8천만 줄을 239개 진입점으로 나누면 진입점당 평균 약 75만 줄이고, 발표의 "전형적으로 60만 줄"과 비슷합니다. 이는 증명이 코드보다 훨씬 크다는 형식 검증의 일반적인 특성입니다.

효율 개선의 신호는 따로 있습니다. 36개의 작은 검증 과제에서 Opus 5.5가 절반을 증명했고, Opus 5보다 토큰을 약 40% 덜 썼습니다. 에이전트들이 서로의 증명을 복사할 수 있게 하자 전체 토큰이 17% 줄었습니다. 이는 "모델이 좋아지면 증명 단가가 내려간다"는 방향의 근거이지, 특정 프로젝트의 견적이 아닙니다.

팀 입장에서 병목은 증명 줄 수가 아니라 명세 작성과 패치 검토입니다. 어떤 속성을 세울지, 어떤 입력 크기까지 책임질지, 실패한 입력을 실제 버그로 볼지 결정하는 일은 자동화되지 않습니다. 예산을 잡을 때는 모델 토큰보다 이 설계 시간을 먼저 계산하세요.

결론: 보장의 범위를 계약서에 적어라

Anthropic과 Theorem의 결과는 "AI가 증명을 쓸 수 있다"를 넘어, "증명의 범위를 문서로 고정할 수 있다"를 보여줍니다. 123개라는 숫자보다 중요한 것은 239개 진입점, 64MiB, 단일 스레드, RISC-V 정적 바이너리, Rocq 커널이라는 조건입니다.

도입한다면 세 문장을 먼저 쓰세요. 어떤 바이너리를 검증하는가. 어떤 속성을 증명하는가. 어떤 실행 조건을 가정하는가. 이 세 문장에 답하지 못하면, 1억 8천만 줄은 안심의 근거가 아니라 읽지 않은 계약서가 됩니다.

연결되는 유료 강의는 에이전트 하네스·루프·그래프 설계 과정입니다. Rocq나 C/C++ 정형 검증 실습을 원하는 독자에게는 별도 학습 자료가 필요합니다.

함께 읽으면 좋은 글

• Claude Security의 연속 스캔: '고침' 표시와 실제 배포 사이의 간격
• AI 에이전트 보안 입문: 권한 없이 실행하면 안 되는 이유

참고 자료

• Anthropic: LLMs are making formal software verification feasible at a much larger scale
• Theorem: OSS Verify — What gets proven
• Theorem: OSS Verify README
• Theorem: OSS Verify proofs
• Theorem: RISC-V and Linux process semantics