# AlphaProof 코드 및 시그널: 기계 검사 보안 증명 및 신뢰할 수 있는 가정

Published: 2026-11-11

Google DeepMind는 컴파일된 libsignal 명령줄 하니스에 대해 선택된 보안 속성에 대한 기계 검사 증명을 보고합니다. Lean은 증명을 확인하고, 사람은 사양과 가정을 승인합니다. 별도의 비교기는 승인된 목표에 대해 정리와 모든 종속 정의를 확인합니다.

Canonical: https://thedailydiff.dev/ko/video/2026-11-10-signal-machine-proof/

## 이 동영상에서 다루는 내용

- AI 에이전트가 후보 증명을 생성하고, Lean의 커널은 해당 증명이 인간이 승인한 공식 주장을 확립하는지 확인합니다.
- 검증된 목표는 신뢰할 수 있는 의미론 및 암호화 계약을 포함하는 특정 컴파일된 libsignal CLI 하니스입니다.
- 컴파일된 이진 파일을 증명함으로써 해당 이진 파일의 명시된 속성에 대한 신뢰 기반에서 Rust 컴파일러가 제거됩니다.
- 연구원들은 이전에 수정된 버그 중 두 가지가 상징적 보안 정리를 위반하는 방식으로 개별적으로 다시 도입되었다고 보고했습니다.
- 비교기는 정리와 모든 종속 정의를 보호된 승인된 사양에 대해 확인합니다. 수정 사항은 별도의 검토 프로세스를 거칩니다.

## 자주 묻는 질문

### AlphaProof Code는 Signal의 구현에 대해 무엇을 증명했습니까?

Google DeepMind는 컴파일된 libsignal 명령줄 하니스에 대해 선택된 보안 속성에 대한 검사된 증명을 보고합니다. 기술 논문은 명시된 모델 하에서 메시지 기밀성 및 인증, 전방향 비밀성 및 침해 후 보안을 다룹니다. 이 결과는 공격자, 세션 및 암호화 가정에 대한 조건을 유지합니다. 그 범위는 모든 Signal 애플리케이션 또는 설치에 대한 포괄적인 보장을 제외합니다.

### AI 생성 보안 증명이 무엇을 확립해야 하는지 누가 결정합니까?

인간 검토자는 사양과 그 가정을 승인합니다. Google DeepMind의 기술 논문은 인간의 지도를 받아 사양 초안을 작성하는 에이전트와 진술이 의미 있는 보안 속성을 포착하는지 테스트하는 검토자를 설명합니다. Lean은 결과 증명의 논리를 확인합니다. 인간은 강력한 목표를 선택하고, 가정을 검토하며, 승인된 사양에 대한 제안된 변경 사항을 판단할 책임이 있습니다.

### Rust 컴파일러를 신뢰하는 대신 컴파일된 기계 코드를 검증하는 이유는 무엇입니까?

컴파일된 이진 파일에 대한 증명은 해당 아티팩트에 대해 명시된 속성을 직접 확립합니다. Google DeepMind의 논문은 해당 속성 중 하나를 위반하는 컴파일러 오류가 정리를 거짓으로 만들 것이라고 설명합니다. 따라서 Rust 컴파일러는 이 주장에 대한 신뢰 기반에서 벗어납니다. 증명은 여전히 명령어 모델, Lean의 커널 및 명시된 암호화 계약을 신뢰합니다.

### 비교기는 증명 에이전트가 목표를 약화시키는 것을 어떻게 막습니까?

비교기는 정리와 그것이 의존하는 모든 정의를 보호된 승인된 사양에 대해 확인합니다. Google DeepMind의 논문은 증명 에이전트가 그 보류된 복사본에 쓸 수 없다고 말합니다. 검사기는 또한 허용된 공리를 확인하고 새로운 커널에서 증명을 다시 실행합니다. 제안된 사양 수정은 별도의 검토 프로세스를 따르며, 인간은 목표의 강도에 대한 책임을 유지합니다.

### The Daily Diff의 검사된 증명 워크플로에 대한 평결은 무엇이었습니까?

The Daily Diff의 평결은 SHIP IT였습니다. Niko는 승인된 주장이 답변을 생성하는 에이전트와 분리되어 있기 때문에 검사된 증명 워크플로를 배포할 것입니다. 그는 모든 결과에 범위와 가정을 첨부할 것입니다. 이 에피소드는 Google이 게시한 증명 아티팩트를 독립적으로 재구축하지 않고 보고하며, 이러한 증거 경계 내에서 워크플로를 승인합니다.

## 챕터

- 0:00 AI 보안 증명은 누가 검사하는가?
- 0:57 주장은 어떻게 증명 대상이 되는가?
- 1:39 컴파일된 이진 파일을 증명하는 이유는 무엇인가?
- 2:16 어떤 보안 속성이 구현 간극에서 살아남았는가?
- 2:59 사양이 깨진 코드를 거부할 수 있는가?
- 3:36 정확한 증명이 잘못된 질문에 답할 수 있는가?
- 4:13 움직이는 목표물을 무엇이 잡아내는가?
- 4:53 이 증명 워크플로를 배포할 것인가?

## 번역된 스크립트

원래 영어 내레이션에서 번역되었습니다. 사용 가능한 오디오 및 캡션은 YouTube에서 제어합니다.

### AI 보안 증명은 누가 검사하는가?

0:00 AI 보안 감사라는 말은 여전히 챗봇을 신뢰하는 것처럼 들립니다. Google의 새로운 Signal 결과는 별도의 커널이 수학적 증명을 제공합니다. 확인합니다. 이 비디오에서 Google은 무엇을 증명했습니까? 그리고 그들은 에이전트가 목표물을 움직이는 것을 어떻게 막습니까? 여기 유용한 답변이 있습니다. 모델은 후보 증명을 작성하고, Lean은 선택된 컴파일된 코드에 대한 인간이 승인한 주장에 대해 증명을 확인합니다. 인간은 여전히 주장과 가정을 소유합니다.

0:21 모델의 승리 연설을 믿지 않고도 결과를 확인할 수 있습니다. 별도의 확인을 통해 조용히 질문이 바뀌는 것을 잡아냅니다. 정의까지 따라가 보겠습니다. 11월 10일 화요일, The Daily Diff입니다. AlphaProof Code는 Google의 소프트웨어 사양 작성을 위한 프레임워크입니다. 인간의 지도를 받아 AI 에이전트로 확인된 증명을 생성합니다. 이 연구는 Signal의 메시징 프로토콜을 구현하는 Rust 라이브러리인 libsignal을 특정 명령줄 프로그램 내에서 대상으로 합니다.

0:45 Google은 오늘 이 작업을 발표했습니다. 그들의 논문은 5명의 연구원이 4주 이상 작업했다고 말합니다. 에이전트가 증명을 작성하는 동안, 인간은 대부분의 노력을 사양에 쏟았습니다. 요구사항은 더욱 비싼 회의가 되는 방법을 찾았습니다. 사양은 프로그램이 무엇을 해야 하는지,

### 주장은 어떻게 증명 대상이 되는가?

0:59 공격자가 무엇을 제어하는지, 그리고 인수가 어떤 가정을 필요로 하는지 명시합니다. 검토자들은 그것이 사람들이 중요하게 생각하는 보안을 포착하는지 묻습니다. 약한 질문에 대한 아름답게 확인된 답변은 그 질문을 그대로 둡니다. 이 팀은 Signal의 핸드셰이크와 메시지 키 래칫에 대한 이전 연구를 기반으로 합니다. 형식적 분석은 이미 이러한 디자인을 연구했습니다. Google의 주장은 그들의 보안 인수를 수정되지 않은 프로덕션 라이브러리의 컴파일된 구현과 연결합니다. 여기서 디자인은 실제 코드와의 접촉에서 살아남아야 합니다. Signal의 최고 기술 책임자 Ehren Kret은

1:27 이전 검증의 더 작은 범위를 넘어 확장된 것을 설명합니다. 구현 세부 사항에는 순서가 뒤바뀐 메시지 및 지연된 메시지를 위한 보관된 세션이 포함됩니다. 실제 소프트웨어는 당신의 우아한 다이어그램이 버린 영수증을 보관합니다. 연구원들은 수정되지 않은 Rust 라이브러리를 표준 컴파일러로 컴파일하여

### 컴파일된 이진 파일을 증명하는 이유는 무엇인가?

1:41 Arm 64비트 Linux 실행 파일을 만듭니다. 그들의 정리는 공식 명령어 모델을 사용하여 해당 이진 파일을 설명하며, 소스 코드와 최적화된 기계 코드 사이의 간극을 넘어섭니다. 명시된 속성을 깨는 컴파일러 오류는 그 정리를 거짓으로 만들 것입니다. 따라서 컴파일러는 이 이진 파일에 대한 신뢰 기반에서 벗어납니다. 당신은 여전히 명령어 모델과 Lean의 검사기를 신뢰합니다. 신뢰 경계가 이동했으며, 그 경계에는 주소가 있습니다. 약 650만 줄의 검사된 증명은 대략 2만 6천 줄의 신뢰할 수 있는

2:06 사양 및 명령어 의미론에 기반합니다. 이것은 아티팩트 개수입니다. 이것들을 지능 점수로 취급하는 것은 개발자를 그들의 노드 모듈 폴더 크기로 순위를 매기는 것과 같습니다.

### 어떤 보안 속성이 구현 간극에서 살아남았는가?

2:16 인수는 메시지 기밀성 및 인증을 다루며, 명시된 모델에 따라 전방향 비밀성 및 침해 후 보안을 포함합니다. 이 마지막 두 가지는 도난된 키 손상에 대한 제한 및 새로운 교환 후 복구를 설명합니다. 각 보장은 공격자 및 세션에 대한 조건을 가집니다. 암호화 프리미티브는 신뢰할 수 있는 계약 뒤에 있습니다. 증명은 이러한 루틴이 명시된 대로 작동한다고 가정하며 암호화 보안 가정에 의존합니다. 한 증명은 암호화를 이상화하고, 다른 증명은 공격자 성공 확률에 대해 추론합니다.

2:42 두 가지 모두 다루는 시나리오에 제한이 있습니다. 어떤 빌드, 어떤 속성, 어떤 가정을 물어보십시오. 이 결과는 연구원들의 명령줄 하니스에 관한 것입니다. 그룹 메시징은 미래 작업이며, 계산 모델은 다중 장치 상태를 제외합니다. 모든 Signal 설치가 버그 없다고 말하는 것은 정리 밖의 일입니다. 연구원들은 이전에 수정된 두 가지 Signal 버그를 격리된 복사본에 다시 도입하고

### 사양이 깨진 코드를 거부할 수 있는가?

3:02 컴파일했습니다. 확인된 증명은 해당 이진 파일이 상징적 보안 정리를 위반했음을 보여주었습니다. 이것은 사양이 실제 손상된 구현을 거부할 수 있는지 테스트했습니다. 당신의 녹색 체크표시는 빨간색 테스트가 필요합니다. Google은 확인 지침과 함께 사양 및 증명을 게시합니다. 리포지토리는 클린 빌드가 몇 시간과 상당한 메모리를 필요로 한다고 말합니다. 발표문을 읽는 것이 노트북에서는 훨씬 더 쉽습니다. 하드웨어 모델과 신뢰할 수 있는 계약은 여전히 검토가 필요합니다.

3:26 이 에피소드를 위해 거대한 아티팩트를 다시 빌드하지 않았습니다. 우리는 게시된 결과와 그 경계를 보고합니다. 외부인들이 그것을 검사할 수 있는 경로가 있으며, 이는 또 다른 AI 승리보다는 저에게 더 중요합니다. 이제 함정입니다.

### 정확한 증명이 잘못된 질문에 답할 수 있는가?

3:36 Lean은 거의 아무것도 요구하지 않는 진술에 대한 올바른 증명을 받아들일 수 있습니다. 불가능한 가정은 정리를 공허하게 만들 수 있습니다. 헤드라인 정리 아래에 숨겨진 정의를 변경하면 목표를 약화시킬 수 있습니다. 논문은 이에 대한 검사를 설계합니다. 게이트키퍼는 증명 에이전트가 작성할 수 없는 보류된 승인된 사양을 유지합니다. 그들은 별도의 수정 프로세스를 통해 수정 사항을 제안할 수 있습니다. 보안 약화는 잠재적 버그로 에스컬레이션됩니다. 증명자의 성공 선언은 여기에서 권한이 없습니다.

4:00 인간은 신뢰할 수 있는 가정의 변경 사항을 직접 또는 정책을 통해 판단하고, 각 캠페인 후 수정 사항을 검토합니다. 전문가의 판단은 책임에 남아 있습니다. 에이전트는 다른 할당을 요청할 수 있습니다. 자신에게 합격점을 줄 수는 없습니다.

### 움직이는 목표물을 무엇이 잡아내는가?

4:13 여기 약속된 확인이 있습니다. Lean의 비교기는 정리와 그것이 의존하는 모든 정의를 보호된 승인된 복사본과 비교합니다. 또한 허용된 공리를 확인하고 새로운 커널에서 증명을 다시 실행합니다. 따라서 도우미 정의를 조용히 약화시키는 것은 비교되는 대상을 변경합니다. 승인된 증명은 승인된 목표를 확립해야 합니다. 여전히 인간은 강력한 목표와 정직한 가정을 선택할 책임이 있습니다. 자신의 AI 워크플로의 경우, 작업자의 편집 권한 밖에 승인 기준을 유지하고

4:37 제안된 변경 사항을 별도로 검토하십시오. Google의 결과는 이러한 분리를 구체화합니다. 증명 작성자는 작업을 수행합니다. 확인 경계가 그것이 유효한지 결정합니다. 이것을 읽는 것을 더 좋아하시면, 매일 아침 당신의 받은 편지함으로 무료로 The Daily Diff가 도착합니다. daily diff dot dev에서 링크를 확인하세요. 그래서 오늘의 평결은 SHIP IT입니다.

### 이 증명 워크플로를 배포할 것인가?

4:54 저는 이 검사된 증명 워크플로를 배포할 것입니다. 왜냐하면 승인된 주장이 답변을 생성하는 에이전트와 분리되어 있기 때문입니다. 저는 모든 결과에 범위와 가정을 첨부할 것입니다. 구독하고, 알림을 켜고, 다르게 스탬프를 찍었을지 댓글로 알려주세요. 오늘의 The Daily Diff였습니다. 저는 Axrisi의 Niko입니다. 책임감 있게 병합하세요.

## 출처

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub