AlphaProof 코드, Signal 암호의 정확성을 입증 — 컴파일된 바이너리 수준에서

인간의 작성 도움 없이 에이전트 팀이 4주 만에 생산한 650만 줄의 Lean 코드. 이것이 2026년 11월 10일 Google DeepMind가 AlphaProof Code를 위해 발표한 대표 수치입니다. AlphaProof Code는 형식 검증을 위한 에이전트 프레임워크로, 연구소는 이를 사용해 Signal 프로토콜의 암호학적 핵심을 기계 검증했으며, 이례적으로 그 위의 설계 문서가 아니라 컴파일된 AArch64 바이너리 수준에서 검증했습니다. 그 작업을 수행한 모델들은 별개의 문제입니다. 공급자 정가 기준 0% 마크업으로 제공되는 API 키 하나 증명 에이전트의 엔진은 저희가 제공하는 대상이 아닙니다.

이 프레임워크는 호출할 수 있는 모델이 아니다. 그것은 하네스다: 인간 전문가들이 무엇이 참이어야 하는지를 결정하고, 여러 모델의 조합이 그 목표들을 Lean 명세로 바꾸며, 그다음 증명 작성 에이전트 팀들이 — 블로그에서는 G​emini Carbon을 엔진이라고 부른다 — Lean의 커널이 받아들일 때까지 증명을 채운다. 발표와 함께 공개된 것은 github.com/google-deepmind/code-verification에 있는 아티팩트 세트와, 결과의 경계에 관해 블로그 글보다 훨씬 솔직한 기술 논문이다. 뒤따르는 내용 대부분은 그 논문에서 나온다. 흥미로운 수치들이 바로 그 논문에 있기 때문이다.

실제로 무엇이 입증되었으며, 무엇을 상대로 입증되었는가

대상은 libsignal v0.105.4와 spqr v1.6.0이며, 표준 rustc 1.98.1로 빌드되고 musl에 정적으로 링크되어 단일 AArch64 Linux 실행 파일로 출력됩니다. 이 세부 사항은 어떤 벤치마크보다 중요합니다. 증명은 컴파일러가 충실히 변환할 것이라고 신뢰하는 Rust 함수가 아니라, 휴대폰에서 실행될 바이트에 관한 것이기 때문입니다. 팀은 약 560KB의 libsignal 소스와 약 140,000개의 AArch64 명령어를 검증했으며, 명령어 집합에 대한 Lean 모델(7,578줄에 걸쳐 467개 명령어와 31개 시스템 호출)을 작성한 다음, 해당 모델 아래에서 로드되고 실행되는 실제 ELF 이미지가 보안 속성을 보존함을 증명함으로써 이를 수행했습니다.

이 속성들은 프로토콜 엔지니어라면 요구할 만한 것들입니다. 열 개의 기호적 정리는 전방 비밀성, 침해 후 보안, 개시자 및 응답자 비밀성, 인증, 그리고 PQXDH의 정리 1에 대한 다섯 개의 따름정리를 다룹니다. 주요 결과의 이름은 signal_session_secure_placed입니다. 또한 구체적인 경계가 있는 계산적 트랙도 있으며, 두 트랙은 서로 다른 적대자 모델을 사용합니다. 기호적 측면(DyLean 프레임워크를 통한 Dolev–Yao)은 핸드셰이크 후에 Diffie–Hellman을 깨는 양자 공격자까지 포괄하는 반면, 계산적 측면은 고전적 적대자만 포괄합니다.

600만 줄은 어디로 가는가

"600만 줄 이상"은 블로그의 표현으로 정확하지만 거칠다. 논문의 세부 분류가 유용하며, 이는 자랑이 아니라 비용 표로 읽을 가치가 있다:

• 바이너리에 대한 증명 — 530만 줄, 작업량의 대부분을 차지하며, 기계어 의미론과 기호 모델에서 실행 파일까지의 정련을 다룹니다.

• 계산 증명 — 약 860,000줄.

• 기호적 증명 — 약 350,000줄.

• 버그 반박 증명 — 아래에 설명된 두 가지 의도적으로 재도입된 취약점에 대한 약 140,000줄 분량.

• 할당자 증명 — 약 70,000줄.

주석과 빈 줄을 포함하면 거의 700만 줄인데, 논문은 포함해 세고 블로그는 포함하지 않는다. 어느 쪽이든 중요한 비율은 증명과 증명된 대상 사이의 비율이다. 560KB 바이너리의 성질을 확립하는 데 650만 줄의 Lean이 사용되었다. 이 비율은 이 기법이 일상적인 것이 되기까지 얼마나 멀리 있는지를 보여 주는 정직한 척도이며, 누군가 형식 검증이 저렴해졌는지 묻는다면 인용해야 할 숫자다.

신뢰 기반은 증명보다 작으며, 바로 그 점이 핵심이다.

증명은 그것이 가정하는 것만큼만 좋습니다. 논문은 이 점을 구체적으로 밝히며, 바로 그 구체성이 이 논문을 보도자료와 구별해 줍니다. 신뢰된 명세는 약 18,000줄(문서 포함 시 28,000줄), AArch64 시맨틱은 약 8,000줄, 기계어의 Lean 인코딩은 약 95,000줄입니다. 37개의 루틴은 검증되는 대신 계약으로 대체됩니다 — SHA-256 및 SHA-512 압축, AES-256-CBC, X25519, Edwards 곡선 연산, Kyber1024 및 ML-KEM-768, 그리고 libcrux HMAC. 18개의 패닉 진입점 역시 증명되는 대신 가정됩니다.

따라서 주장은 "모든 것이 증명되었다"는 것이 아니다. 주장은 암호 프로토콜 로직, 세션 상태 머신, 그리고 그 로직에서 실제로 실행되는 명령어로의 정련이 증명되었으며, 그 아래의 프리미티브들은 모든 검증 프로젝트가 자신의 프리미티브를 신뢰하는 방식으로 신뢰된다는 것이다. 특히 Rust 컴파일러는 신뢰 기반에 없다 — 팀은 기계어 수준에서 추론함으로써 그것을 신뢰할 필요를 피했는데, 이는 검증된 컴파일러를 완전히 우회할 수 있게 해 주는 것과 같은 요령이다. 규모에 대한 참고로, 논문은 seL4를 약 20인년, CompCert를 약 6인년으로 인용한다.

버그 두 개를 일부러 다시 넣었습니다.

검증 시스템이 항상 "correct"라고만 말한다면 테스트할 수 없다. 그래서 팀은 이전에 Signal의 코드에서 발견되어 수정된 두 가지 취약점 — 약한 상태 버그와 작은 부분군 버그 — 을 격리된 복사본에 다시 도입하고 파이프라인을 다시 실행했다. 두 경우 모두 AlphaProof Code는 버그가 있는 버전이 보안 정리를 충족하지 못한다는 기계 검증된 증명을 생성했다. 기호 명제는 ¬Sec(Asm_bug)로 귀결된다.

논문은 마케팅 페이지라면 잘라냈을 주의 단서를 덧붙인다: 그런 버그들에 대한계산적 정리를 반박하는 것은 "훨씬 더 어렵다"며 미해결로 남겨졌다. 다시 말해, 부정 테스트는 기호적 트랙에서는 깔끔하게 작동하고 계산적 트랙에서는 아직 작동하지 않는다. 바로 이것이 독자가 이 프레임워크를 버그 탐지기로 취급하기 전에 알아야 할 종류의 비대칭성이다.

에이전트가 어떻게 실행되었는지

4주에 걸쳐 다섯 명의 연구자가 각자 에이전트를 중단 없이 실행했습니다. 증명 작성 자체는 팀당 40~80개의 에이전트로 구성된 팀이 수행했으며, 팀당 단일 머신에서 24~72시간 동안 실행되었고, 팀 오케스트레이터 위에는 감독 에이전트가 있었습니다. 게이트키퍼 에이전트는 각 제출물을 comparator를 사용해 홀드아웃 명세 사본 및 Lean 커널과 대조해 검사합니다. 이는 에이전트가 요청받은 내용을 미묘하게 약화한 버전을 증명하는 것에 대한 방어책입니다.

인간의 작업은 명세에 집중적으로 배치되었다. 증명 작업이 시작되기 전에 모든 명세는 전문가의 검토를 거쳤고, 에이전트 자체의 감사 패스는 코드베이스의 약 1%를 인간의 주의가 필요하다고 표시했다. 인간이 증명 코드를 작성한 경우는 없었다. 이 논문은 엔지니어링 측면에 대해서도 솔직하다. 클린 빌드는 몇 시간이 걸릴 수 있고, 초기에는 사소한 소스 편집이나 재컴파일된 바이너리 때문에 대규모 증명 수리가 불가피했으며, AI가 생성한 증명과 증명 기법 자체 모두에 "상당한 최적화 여지"가 있다.

증명이 다루지 않는 것

한계점은 논문에서 가장 중요한 절이 될 만큼 길고, 평이하게 서술된다. SPQR의 치유(healing) 속성에 대해서는 포스트 양자 보장이 확립되지 않는다 — 래칫 정리들은 공격자가 SPQR 키를 선택한다고 가정한다. 페이로드 프라이버시는 증명되지 않는다. 절대 승격되지 않는 핸드셰이크의 첫 메시지에 대해서는 응답자 인증이 증명되지 않는다. 모델은 승격당 하나의 세션, 고정된 메시지 길이, 다중 기기 상태 없음, 그리고 최초 사용 시 신뢰(TOFU) 방식의 신원 키를 허용한다.

또한 공허해지는 상한도 있다. 8바이트 MAC 위조 항은 시도당 최소 2⁻⁶⁴이며 메시지와 에포크에 대해 제곱으로 증가하는데, 이는 약 25,000개 메시지의 단일 세션 또는 2¹⁰개 메시지의 2²⁰개 세션에 대해서는 그 상한이 더 이상 아무것도 말해 주지 않게 됨을 뜻한다. 그리고 증명의 대상은 새 프로세스로 실행되는 팀의 libsignal-cli 빌드이지, 휴대폰의 Signal 앱이 아니다. 몇 가지 환경 가정은 증명되지 않고 비형식적으로 논증된다.

API도, 가격도, 호출할 모델도 없습니다.

모델 리더보드에서 넘어온 사람이라면 누구든 실망할 부분이 바로 이것이다. AlphaProof Code는 연구 프레임워크이자 공개된 아티팩트 세트다. 엔드포인트도, 토큰당 요금표도, 대기자 명단도, 가중치도 없다. 저장소에는 체크포인트가 아니라 Lean 개발, AArch64 시맨틱스, libsignal 바인딩 및 명세가 들어 있다. 블로그에서는 아티팩트가 오픈소스로 공개되었다고 말하지만, 랜딩 페이지에는 라이선스가 명시되어 있지 않으며, 그 위에 무언가를 구축할 계획이라면 이 점을 확인해 볼 가치가 있다.

작업을 수행한 모델은 별개의 문제입니다. 논문은 증명 에이전트로 Gemini 4 Carbon을 지목하고, 사양 초안 작성과 검토에는 다른 모델들과 함께 Claude Opus 5.5가 사용되었다고 밝힙니다. Claude Opus 5.5는 현재 OrcaRouter 카탈로그에 입력 토큰 100만 개당 4달러, 출력 토큰 100만 개당 20달러로 등재되어 있으며, 공급자 정가가 0% 마크업으로 그대로 전달됩니다. 따라서 원하시는 실질적 시사점이 "논문에서 사용한 모델로 사양 초안 작성 루프를 돌려라"라는 것이라면, 그 부분은 평범한 API 호출이며, 공급업체의 가격이 바뀌면 당일 저희 쪽에 반영됩니다. 증명 에이전트의 엔진은 저희가 제공하는 것이 아니며, 여기서 AlphaProof Code 자체를 호스팅한다는 의미는 아닙니다.

왜 이것이 Signal 결과보다 더 큰 사안인가

Signal 검증은 그 자체로 인상적이다 — DeepMind에 따르면 AI 사용 여부와 관계없이 어떤 방법으로든 널리 배포된 프로토콜의 구현을 형식 검증한 최초의 사례이며, AI가 배포된 암호 프로토콜을 이 정도 깊이로 검증한 것도 처음이다. 그러나 더 널리 적용할 수 있는 핵심은 워크플로다. 5명으로 구성된 팀이 4주 만에, 명세 검토 단계와 에이전트 게이트키퍼를 갖추고, 예전 같으면 수년짜리 프로젝트였을 증명 코퍼스를 만들어냈다. 이 비율이 느슨하게라도 유지된다면, 검증을 감당할 수 있는 시스템의 범위가 달라진다. 의료기기 펌웨어, 전력망 소프트웨어, 지금은 코드 리뷰와 기도 한 번으로 끝나는 부류의 코드까지.

그것이 성립하는지는 검증되지 않았다. Signal의 암호는 유난히 잘 명세되어 있고, 팀은 Signal 자체 엔지니어들에게 방법론을 검토받았으며, 프리미티브는 검증된 것이 아니라 외부에 위탁되었다. 다음 시스템은 그렇게 협조적이지 않을 것이다. 논문 자체의 틀, 즉 형식 검증을 CodeMender 같은 자동화된 방어 에이전트와 짝지우라는 것은 그 제안의 정직한 형태다. 검증은 무엇이 참인지 알려주고, 참이 아닌 것을 고치는 일은 다른 무언가가 해야 한다.

무엇을 볼까요?

세 가지가 있다면 이것을 획기적인 논문에서 산업적 기법으로 끌어올릴 것이다. Google 외부의 누군가가 검증한 두 번째의 독립적인 코드베이스, 이상적으로는 기존 분석에서 각색한 것이 아니라 명세를 처음부터 작성해야 했던 코드베이스. 비용 수치 — 에이전트-시간, 가속기-시간, 달러 — 이다. 4주와 40~80명의 에이전트 팀은 어떤 엔지니어링 관리자도 예산을 세울 수 있는 단위가 아니기 때문이다. 그리고 계산 트랙의 버그 반박인데, 이는 논문이 열린 문제로 남겨 둔 것이며 속성을 증명하는 시스템과 특정 바이너리가 깨졌다고 계산적으로 알려줄 수도 있는 시스템 사이의 차이다.

그때까지는 공지문 대신 아티팩트 저장소를 읽으세요. 증명이 거기에 있고, Lean이 그것을 검사하며, 논문은 그것들이 무엇을 전제하는지 정확히 알려 줍니다.