AlphaProof Code: Signal 기계어 검증에서 명세와 증명의 역할

Google DeepMind는 2026년 11월 10일 AlphaProof Code를 발표했다. 연구진은 이 프레임워크로 Signal 프로토콜 구현의 보안 속성을 기계어 수준에서 증명했다고 밝혔다. 개발자가 살펴볼 부분은 AI가 쓴 증명과 사람이 승인하는 명세의 역할 분담이다. 공식 발표에서 연구 목적과 결과를 확인할 수 있다.

명세를 승인하는 사람과 증명을 쓰는 에이전트

AlphaProof Code에서는 사람이 AI와 함께 보안 목표를 Lean 명세로 옮긴다. 사람이 명세를 승인하면 증명 에이전트들이 구현이 그 명세를 만족하는지 증명한다. Lean 커널이 증명을 검사한다. comparator는 승인된 명세와 증명 대상이 일치하는지 확인한다.

AI가 논리적으로 틀린 증명을 내면 Lean이 거부한다. 다만 명세 자체가 약하거나 전제가 잘못되면 검사를 통과한 증명도 원래 원하던 보장을 주지 못한다. 논문은 명세를 검토하고 최종 판단을 내리는 사람의 역할을 남겨 둔다. 이 구조는 기술 보고서 2절에 설명돼 있다.

검증 대상은 특정 버전과 실행 환경

연구진은 수정하지 않은 libsignal v0.105.4와 spqr v1.6.0을 작은 명령행 프로그램에 연결했다. 검증 대상은 이를 컴파일한 AArch64 Linux 실행 파일이다. 연구는 일대일 세션의 PQXDH와 Triple Ratchet을 다룬다. 그룹 메시징은 범위에서 제외했다.

보고서는 상징적 모델과 계산적 모델의 보장을 구분한다. 일부 암호 기본 연산은 계약으로 명세하며 해당 연산의 성질과 실행 환경에는 신뢰해야 할 가정이 남는다. 따라서 이 결과를 Signal 앱 전체나 모든 기기 환경의 안전성 보장으로 넓혀 읽을 근거는 없다. 구체적인 경계는 공개 명세와 증명 문서의 4·5절에서 확인할 수 있다.

4주와 증명 코드 규모의 의미

연구진은 5명이 4주 동안 증명 작업을 진행했다고 보고했다. 약 650만 줄의 Lean 증명 코드를 만들었고 신뢰해야 하는 명세와 AArch64 의미론은 약 2만 6,000줄이라고 설명한다. 이 수치는 연구진의 보고이며 독립 재현 결과는 이번 조사에서 확인하지 못했다.

팀은 이미 수정된 실제 버그 2개를 격리된 코드에 다시 넣었다. 두 경우 모두 버그가 들어간 구현이 안전하지 않다는 기계 검증 증명을 얻었다고 밝혔다. 새 취약점 2개를 발견했다는 발표와는 구별해야 한다. 공식 발표와 기술 보고서 6·7절이 이 실험을 설명한다.

개발팀이 공개 자료를 읽는 순서

자체 코드에 적용할 방식을 검토한다면 증명할 속성과 제외할 범위를 먼저 정해야 한다. 이 사례에서는 승인한 명세, 그 명세가 가정하는 암호 연산, 검증한 실행 파일의 관계를 따라 읽을 수 있다. 검토할 때는 증명 코드의 줄 수와 함께 명세의 범위를 확인해야 한다.

DeepMind는 공식 저장소와 문서를 공개했다. 이번 글에서는 공개 문서를 대조했으며 전체 증명을 직접 빌드하거나 재검사하지 않았다.