# Claude 형식 검증 — 끝난 증명 베껴 쓰기

> 앤트로픽이 Claude로 오픈소스 123개에 «안 멈춘다»를 증명한 연구를 읽고, 그 안의 «끝난 증명 베껴 쓰기» 하나를 제 게임 스튜디오 아트팀에 붙여 전후를 쟀습니다.

- 수치: 시간 −21% · 비용 그대로
- 사람이 보는 화면: https://aitryed.com/ko/teardowns/qa/formal-verification/
- 반대 언어: https://aitryed.com/en/teardowns/qa/formal-verification/index.md
- 출처(앤트로픽 연구 글 (2026-10-22)): https://www.anthropic.com/research/formal-verification
- 출처(소개한 인스타그램 글 (ai.asap.kr)): https://www.instagram.com/p/De5VM-zE0Xz/
- 이 사이트 안내(AI용): https://aitryed.com/ko/llms.txt

---

**앤트로픽이 Claude에게 오픈소스 라이브러리 123개를 맡겨, 그 안의 시험 입구 239곳이 «64MB보다 작은 어떤 입력을 넣어도 멈추지 않는다»는 것을 수학으로 증명하게 한 연구입니다.** 이걸 형식 검증이라고 부릅니다. 저는 그중 한 대목, «다른 에이전트가 끝낸 증명을 베껴 쓰게 했더니 토큰이 17% 줄었다»를 제 게임 스튜디오 아트팀에 붙여 봤습니다. 시간은 21% 줄었고, 비용은 그대로였습니다.

> **[도판]**
>
> 퍼징과 형식 검증의 차이. 퍼징은 시험 입구에 무작위 입력을 계속 넣어 멈추는 입력을 찾는다. 형식 검증은 같은 입구를 명세로 바꾸고 Claude가 쓴 증명을 Rocq가 채점한다.

## 「무작위로 많이 넣어 보기」와 「전부 괜찮다고 증명하기」는 다른 일입니다

프로그램에 버그가 있는지 보는 흔한 방법은 **퍼징**입니다. 아무 입력이나 수없이 넣어 보고, 프로그램이 멈추는 순간을 찾습니다. 오래 돌릴수록 많이 찾습니다. 그런데 넣을 수 있는 입력은 끝이 없어서, 아무리 돌려도 «안 넣어 본 입력»이 남습니다.

형식 검증은 방향이 반대입니다. 하나하나 넣어 보는 대신, **«어떤 입력이 와도 이 프로그램은 멈추지 않는다»를 수학 증명으로 씁니다.** 증명이 맞는지는 사람이 아니라 검사 프로그램(여기서는 Rocq)이 한 줄씩 채점합니다.

문제는 이 증명이 엄청나게 길다는 것이었습니다. 운영체제 커널 하나를 만드는 데 2인년, 그걸 증명하는 데 20인년이 걸린 예가 있습니다. 그래서 지금까지는 비행기 제어 코드 같은 아주 중요한 곳에서만 했습니다.

## 이번 연구가 바꾼 것 — 증명을 쓰는 일을 Claude가 맡았습니다

앤트로픽은 이미 있던 퍼징 시험을 그대로 «약속»으로 바꿨습니다. «이 시험 입구는 64MB보다 작은 어떤 입력에도 멈추지 않는다.» 그리고 Claude가 그 약속의 증명을 썼습니다.

| 숫자 | 뜻 |
|---|---|
| 123개 · 239곳 | 증명한 라이브러리 수 · 시험 입구 수 |
| 약 1억 8천만 줄 | 쓴 증명 전체. 한 편이 보통 60만 줄 |
| 몇 주 | 걸린 기간 |
| 수백 개 | 증명하다가 찾은 버그. 수조 번 퍼징에서 안 나온 것도 있었다 |

증명이 막히면 그 자리에 버그가 있다는 신호입니다. Claude는 버그를 고치고, 고친 코드로 다시 증명했습니다. 예를 들어 20MB쯤 되는 특정한 모양의 입력에서만 터지는 버그가 있었습니다. 퍼저는 보통 1MB 넘는 입력을 안 넣어서 못 찾던 것입니다.

## 「증명됐다」는 「버그 0개」가 아닙니다

글이 직접 선을 그었습니다. 증명은 «약속을 지킨다»는 뜻이지, 그 약속이 현실과 맞는다는 뜻이 아닙니다.

이번 약속은 몇 가지를 깔고 있습니다. 한 줄로만 도는 프로그램, RISC-V라는 칩, 리눅스입니다. 그런데 대부분의 사람은 같은 라이브러리를 x86이나 ARM 칩에서 돌립니다. 그 차이만큼은 증명 밖입니다. 그래서 남은 버그가 있다면 **어디를 봐야 하는지**는 알게 됐다고 글은 말합니다. 약속 자체, 칩과 운영체제를 흉내 낸 모형, 채점 프로그램 셋입니다.

## 제가 가져온 건 증명이 아니라 「서로 베껴 쓰기」입니다

저는 증명을 쓸 일이 없습니다. 대신 글 뒤쪽의 한 실험이 눈에 걸렸습니다.

에이전트 여럿이 각자 다른 증명을 쓸 때, **서로의 끝난 증명을 베껴 갈 수 있게** 공유 작업장을 열어 줬습니다. 그랬더니 혼자 쓸 때보다 토큰이 17% 덜 들었고, 혼자서는 실패하던 것이 성공하기도 했습니다. 이유도 적혀 있었습니다. 프로그램마다 증명의 대부분은 «어느 프로그램에나 있는 부분»이라서, 남의 것을 가져와 고치면 된다는 것입니다.

제 스튜디오에도 똑같은 모양이 있을 것 같았습니다. AI가 도트 애니메이션을 만들 때, 그림을 그리는 대본 말고도 비교 시트를 만들고 확대해 보고 점검하는 대본을 매번 씁니다. 그건 어느 캐릭터에나 있는 부분입니다.

## 재 보니 84%를 매번 새로 쓰고 있었습니다

먼저 지금 상태를 쟀습니다. 아트팀이 지금까지 남긴 대본 2만 1천여 줄을, 먼저 만든 대본과 줄 단위로 맞대 봤습니다.

| | 줄 | 비율 |
|---|---|---|
| 새로 쓴 줄 | 18,012 | 84% |
| 그대로 · 조금 고쳐 다시 쓴 줄 | 3,306 | 16% |

다시 쓴 16%도 거의 전부 **같은 세션이 자기 것을 이어 쓴 경우**였습니다. 다른 세션이 만든 대본은 거의 안 가져다 썼습니다. 그리고 새로 쓴 줄 가운데 7,450줄은 그림이 아니라 보기 · 비교 · 점검 도구였습니다.

## 그래서 붙이고, 같은 일을 둘로 나눠 돌렸습니다

앞서 끝난 대본 111개를 작업별로 묶은 목록 한 장을 만들었습니다. 그리고 같은 일을 네 번 시켰습니다.

- 일: 윈디(네 발)와 괴력몬(두 발)이 쓰러지는 애니메이션 4장씩
- A조 2명: 지금 방식 그대로
- B조 2명: «대본을 쓰기 전에 이 목록에서 같은 일을 한 대본을 찾아 베껴 고쳐 쓰라»
- 같은 모델, 같은 노력 단계, 같은 시각에 따로 돌렸습니다

## 결과 — 덜 쓰고 빨리 끝났지만, 돈은 그대로였습니다

> **[도판]**
>
> A조와 B조 비교 막대. 새로 쓴 대본 줄은 86퍼센트에서 19퍼센트로, 걸린 시간은 10분 30초에서 8분 14초로, 출력 토큰은 5만 8천에서 4만 8천으로 줄었다. 전체 비용은 93만에서 91만으로 거의 같았다.

B조는 새로 쓴 줄이 86%에서 19%로 줄었습니다. 시간은 21%, AI가 내놓은 글자(출력 토큰)는 19% 줄었습니다. 앤트로픽이 잰 17%와 거의 같은 크기입니다.

그런데 전체 비용은 거의 같았습니다. 베껴 온 대본을 읽느라 **읽는 쪽 토큰이 늘어서**, 덜 쓴 만큼을 거의 다 도로 냈습니다. 그림은 넷 다 기계 점검을 통과했습니다. 눈으로 보면 한 장씩 흠이 있었는데(B조 윈디는 누운 몸통이 떠 보였습니다), 조 사이 우열은 보이지 않았습니다.

그래서 스튜디오에는 붙여 두었습니다. 같은 돈으로 더 빨리 끝나기 때문입니다. 다만 «토큰을 아끼는 방법»으로는 이번 측정에서 증명되지 않았습니다.

## 못 한 것

- **표본이 두 쌍뿐입니다.** 같은 A조끼리도 비용이 1.7배 차이 났습니다. 앤트로픽은 36개 과제를 세 번씩 돌렸습니다. 제 숫자는 방향만 보여 주고 크기는 못 믿습니다.
- **그림 수준은 아직 사람이 안 봤습니다.** 기계 점검 통과는 «결함이 없다»까지입니다.
- **B조가 지적한 목록 결함 둘을 고쳐서 붙였습니다.** 한 작업의 대본이 여러 절로 흩어져 있던 것, 베낀 대본의 기본값이 다른 기준에 맞춘 값이라는 걸 알 길이 없던 것입니다. 고친 목록으로는 아직 다시 재지 않았습니다.

## 여기부터는 자세한 기록입니다

**앤트로픽(Frontier Red Team)과 Theorem이 2026-10-22 에 낸 연구다.** OSS-Fuzz 의 퍼징 입구를 «64MB 미만의 어떤 입력에도 크래시하지 않는다»는 명세로 바꾸고, Claude 가 RISC-V 로 컴파일된 실행 파일 수준에서 그 증명을 썼다. 123개 라이브러리 · 239개 입구가 증명됐다. 나는 이 글에서 «증명 재사용» 실험 하나를 골라 문스튜디오 아트팀(도트 애니메이션 에이전트)에 옮기고, 2종 × 2조로 전후를 쟀다.


## 원문이 말한 것 — 숫자와 조건

원문의 주장은 «LLM 이 형식 검증을 훨씬 큰 규모에서 할 수 있게 만들고 있다»이다. 근거로 든 수치를 그대로 옮긴다.

| 항목 | 값 |
|---|---|
| 대상 | OSS-Fuzz 라이브러리 123개 · 퍼징 입구 239개 |
| 명세 | 64MB 미만 모든 입력 · 모형화한 모든 리눅스 응답과 메모리 배치에서 크래시 없음 |
| 전제 | 단일 스레드 정적 바이너리 · 고정 메모리 예산 · RISC-V · 리눅스 · musl libc |
| 증명 규모 | Rocq 약 1억 8천만 줄 · 한 편 약 60만 줄 · 바이너리 중앙값 1만 8천 명령 |
| 기간 | 몇 주 |
| 믿어야 하는 것 | RISC-V · 리눅스 프로세스 형식 모형 · 증명한 정리 문장 · Rocq 검사기 |

크래시는 잘못된 메모리 접근, 실패한 assert, 모형에 없는 동작 셋을 뜻한다. 퍼징 시험을 Rocq 로 옮겨 적지 않고 컴파일된 바이너리를 그대로 해석했는데, 옮겨 적다가 생기는 오류를 피하려는 선택이었다.

### 버그가 증명 «과정»에서 나왔다

증명이 막힐 때마다 Claude 가 코드를 고치고 명세를 다시 만든 뒤 다시 증명했다. 수백 개가 나왔다. 원문이 든 예는 넷이다. 20MB 안팎의 드문 배치에서만 나는 압축 해제기의 카운터 언더플로, 64MB 입력과 2GB 넘는 메모리가 있어야 나는 이미지 디코더의 범위 밖 읽기, 한 파일에 대한 두 핸들을 특정 순서로 불러야 나는 읽기, 깊게 중첩된 입력이 필요한 libexpat 의 알려진 취약점 재발견. 퍼저는 보통 1MB 까지만 넣는다.

### 보상 해킹을 원문이 먼저 짚었다

«고치고 다시 증명»에는 구멍이 있다. 프로그램을 «아무것도 안 하는» 코드로 바꾸면 무엇이든 증명된다. 원문은 패치마다 감점을 주고, 바뀌는 입력이 얼마나 적은지 증명하면 가산점을 줬으며, 패치를 기록해 감사했다고 적었다. 내 게이트 운영에서도 같은 모양을 여러 번 겪었다 — 「통과」가 목표가 되면 통과하기 쉬운 쪽으로 대상이 바뀐다.

### 효율 두 가지 — 새 모델, 그리고 재사용

- 실제 OSS-Fuzz 코드로 만든 작은 검증 과제 36개에서, Opus 5.5 는 절반을 Opus 5 보다 약 40% 적은 토큰으로 증명했다(과제당 단일 에이전트 3회 · 500만 토큰 예산).
- 에이전트가 서로의 증명을 복사할 수 있는 공유 작업장에서는 혼자일 때보다 토큰이 17% 덜 들었다. 끝난 34편 중 30편이 혼자 평균보다 쌌고, 혼자서는 못 끝낸 두 편이 끝났다.
- 재사용이 통한 이유도 적혀 있다. 증명의 대부분이 C 런타임 초기화와 AddressSanitizer 처럼 모든 프로그램에 있는 부분이었다.

## 내 환경에 대봤다 — 아트팀 대본의 재사용률

문스튜디오 아트팀은 도트 애니메이션을 Python 대본으로 만든다. 작업마다 `_scripts` 폴더에 대본을 남기고, 규칙에도 «다음 종이 다시 쓴다»고 적혀 있었다. 실제로 다시 쓰는지 쟀다.

**재는 법.** 대본 파일마다, 그보다 먼저 만든 «다른 작업 폴더»의 대본들과 줄 단위로 맞대 가장 비슷한 값을 쓴다. 분류는 원문 그림 6 의 칸을 따랐다 — 같음(99% 이상) · 조금 고침(80~99%) · 많이 고침(40~80%) · 새로 씀(40% 미만).

| 분류 | 줄 | 비율 |
|---|---|---|
| 새로 씀 | 18,012 | 84% |
| 많이 고침 | 1,599 | 8% |
| 같음 | 1,024 | 5% |
| 조금 고침 | 683 | 3% |

대본 115개 · 2만 1,318줄. «같음»은 전부 같은 세션의 다음 판이었다(이펙트 공용 도구 한 벌이 1→2→4→5판으로 이어짐). 몸 애니메이션과 이펙트 사이, 다른 세션 사이의 재사용은 2~10% 수준으로 사실상 없었다. 새로 쓴 줄을 파일 이름으로 가르면 보기 · 비교 · 점검 · 측정 도구가 7,450줄이었다 — 원문이 말한 «모든 프로그램에 있는 부분»에 해당한다.

## 적용 — 공유 작업장 목록 한 장

끝난 대본의 머리말 첫 줄과 «쓰는 법» 줄을 손대지 않고 옮겨 목록 한 장을 만드는 대본을 썼다. 손으로 요약하지 않은 이유는, 요약하는 순간 목록이 대본과 어긋나기 시작하기 때문이다. 처음 판은 대본 111개를 쓰임새(비교 · 보기 · 측정 · 납품 · 뼈대 · 본체)로 묶었다.

### 실험 설계

| | |
|---|---|
| 과제 | 쓰러짐 애니메이션 · 오른쪽 · 4장 안팎 · 부위 움직이기 · 끝 장 유지 |
| 대상 | 윈디(네 발) · 괴력몬(두 발 · 팔 넷) — 둘 다 원작 쓰러짐이 없다 |
| 기준 | 리자몽 원작 쓰러짐 · 기계 점검 · 숫자 거름 다섯 · 비교 시트 |
| A조 | 지금 방식 그대로 |
| B조 | 지시문 맨 앞에 «목록에서 같은 일을 한 대본을 찾아 베껴 고쳐 쓰라» 한 단락 |
| 통제 | 같은 에이전트 정의 · 같은 모델 · 같은 노력 단계 · 같은 시각 · 서로의 폴더는 열지 않게 함 |

토큰은 각 에이전트 기록의 호출별 사용량을 더했다. 비용은 입력 1 · 캐시 쓰기 1.25 · 캐시 읽기 0.1 · 출력 5 의 상대 가중으로 셌다.

### 결과

| | A 윈디 | A 괴력몬 | B 윈디 | B 괴력몬 |
|---|---|---|---|---|
| 새로 쓴 줄 | 86% | 86% | 17% | 21% |
| 시간 | 9분 25초 | 11분 36초 | 8분 50초 | 7분 37초 |
| 출력 토큰 | 54,385 | 62,494 | 50,544 | 44,622 |
| 캐시 쓰기 | 123,167 | 149,208 | 161,935 | 147,529 |
| 상대 비용 | 698k | 1,168k | 1,001k | 816k |
| 기계 점검 | 통과 | 통과 | 통과 | 통과 |

조 평균으로 B 는 시간 −21% · 출력 −19% · 상대 비용 −3% 였다. 캐시 쓰기는 +13% 였다. 이 증가가 베낀 대본을 읽어 들인 몫이고, 출력에서 아낀 만큼을 거의 상쇄했다. 두 B 가 베껴 온 곳은 같았다 — 같은 동작 · 같은 길 · 같은 기준을 먼저 한 거북왕 쓰러짐 작업 한 벌이었다.

### B조가 짚은 목록 결함 둘

- 한 작업의 대본 한 벌이 쓰임새별로 다섯 절에 흩어져 있었다. 둘 다 결국 «작업 한 벌을 통째로» 베꼈으니, 목록의 단위가 틀렸던 것이다. → 작업 단위로 다시 묶었다.
- 베낀 대본의 허용 기본값이 이전 작업 기준(다른 정답지의 4px)에 맞춘 값이었다. 그대로 뒀으면 이번 기준(2px)에서 점검이 떨어질 뻔했다. 대본 안에 그 값의 출처가 없었다. → 목록 머리에 «베낀 기본값은 이번 기준으로 다시 잰다»를 적었다.

## 판정 — 붙였다, 이유는 시간이다

에이전트 정의와 작업 안내에 «대본을 새로 쓰기 전에 목록에서 작업 한 벌을 찾아 베낀다» 한 줄을 넣고, 목록 생성 대본을 같은 폴더에 두었다. 비용이 같고 시간이 줄었으며 품질이 떨어진 증거가 없어서다.

수확은 하나지만 값을 치르고 배운 것이 하나 더 있다. **«덜 쓴다»와 «덜 낸다»는 다른 숫자다.** 출력만 봤으면 «19% 절감»이라고 보고했을 것이다. 읽는 쪽을 같이 더하자 그 절감은 잡음 안으로 사라졌다. 원문의 17% 도 토큰 총량이라, 내 조건에서 그대로 재현됐다고 말할 수 없다. 내 과제는 증명보다 훨씬 짧아서 «읽는 비용»의 비중이 크다는 차이도 있다.

남은 일은 셋이다. 고친 목록으로 다시 재기, 표본을 늘리기, 그림 수준을 사람 눈으로 보기.