연구 논문을 일반인에게 설명하는 YouTube 채널 Two Minute Papers가 DeepMind의 AlphaProof Code를 다뤘는데, 그 바탕이 된 논문은 관심을 받을 만합니다. 핵심 주장은 AI 에이전트가 Signal 프로토콜의 주요 보안 특성을 단순화한 모델이 아니라 실제로 휴대폰에서 돌아가는 기계어 코드에 대해 증명했다는 것입니다. Signal, WhatsApp, Google Messages에 의지하는 사람에게는 실제 버그가 숨어 있기 쉬운 곳이 바로 이 층입니다.
논문은 보도보다 정확합니다. 대상은 Rust로 작성된 참조 구현 libsignal로, 표준 컴파일러로 AArch64 기계어로 컴파일한 뒤 프로세서의 형식 모델과 함께 Lean에 불러왔습니다. 에이전트는 기계 검증된 증명 약 650만 줄을 만들었고, 그 바탕은 약 26,000줄의 신뢰된 명세와 프로세서 의미론입니다. 증명은 양자 이후 PQXDH 핸드셰이크와 Triple Ratchet을 다루며 전방 비밀성, 인증, 침해 이후 보안, 핸드셰이크 비밀성을 입증합니다. DeepMind 블로그에 따르면 작업은 4주가 걸렸고, 사람은 모든 명세와 에이전트가 표시한 코드베이스 약 1%를 검토했습니다.
주장을 믿을 만하게 만드는 것은 설계입니다. 증명을 쓰는 에이전트는 신뢰하지 않는 대상으로 다룹니다. 문지기 역할의 에이전트는 Lean 커널이 증명을 검사하고 비교 도구가 승인된 명세의 보관본을 정확히 증명한다고 확인할 때만 증명을 받아들입니다. 그래서 에이전트가 목표를 몰래 약하게 바꿀 수 없습니다. 비교 삼아 논문은 seL4 마이크로커널 검증에 20인년, CompCert 컴파일러에 6인년이 걸렸고 둘 다 처음부터 검증을 염두에 두고 작성되었다고 짚습니다.
같은 방식이 일반 개발 도구에도 퍼지고 있습니다. 우리가 리뷰한 Lean LSP MCP는 검사기가 받아들이는 증명을 쓰도록 에이전트에게 Lean의 증명 상태와 오류를 전달하는 서버입니다. 이번 에이전트는 Gemini 4 Carbon으로 돌아갔습니다. 중요한 코드에 AI를 쓰는 사람에게 주는 교훈은 모델과 결과 사이에 따질 수 없는 검사기를 두라는 것입니다.
한계는 논문에 적혀 있습니다. 결과는 Lean 커널, 바탕이 되는 암호 기본 요소의 안전성, 코드가 호출하는 일부 루틴의 동작을 신뢰합니다. 증명은 명세가 말하는 것만 다루므로, 그 26,000줄의 신뢰된 부분에 빈틈이 있다면 보장에도 빈틈이 생깁니다. 결과물은 확인을 위해 공개되어 있지만 독립적인 검증은 아직 이뤄지지 않았습니다.