2026년 11월 10일, 구글 딥마인드는 AlphaProof Code를 공개했다. Signal 암호 프로토콜의 실제 코드를 형식 검증한 다중 모델 에이전트 프레임워크다. 널리 쓰이는 암호 프로토콜의 구현 코드를 기계어 수준까지 형식 검증한 것은 AI 사용 여부를 떠나 이번이 처음이다. Gemini Carbon이 이끄는 에이전트들은 600만 줄이 넘는 Lean 증명 코드를 생성했고, 전문가 팀이 수년 걸릴 일을 4주 만에 마쳤다. 사람이 다시 확인할 필요가 있었던 코드는 약 1%에 불과했다.
검증 대상은 Signal 프로토콜의 핵심인 PQXDH 핸드셰이크와 Triple Ratchet으로, 일대일 세션의 초기화·송신·수신을 다루며 전방향 비밀성, 침해 후 안전성, 인증 등의 속성을 증명했다. 핵심은 '구현'이라는 단어다. 기존 검증은 대개 프로토콜 설계 단계에서 멈추는데, 설계와 코드 사이의 틈이 바로 취약점이 숨어 있는 곳이기 때문이다. 이번에는 컴파일된 AArch64 기계어 자체가 증명됐다. 딥마인드는 역방향 검사도 했다. 실제로 존재했다가 나중에 수정된 두 개의 취약점을 격리된 코드에 다시 심었고, 시스템은 두 번 모두 해당 버전이 안전하지 않다는 것을 기계 검증된 증명으로 보여줬다. 검증 결과물과 기술 논문은 오픈소스로 공개됐다.
증명된 것과 증명되지 않은 것
이 증명의 경계는 분명히 해야 한다. 대상은 libsignal 구현 코드와 일대일 세션이며, 그룹 채팅, 키 생성, 다중 기기 상태는 포함하지 않는다. 약 2만 6천 줄의 신뢰할 수 있는 명세와 의미론은 여전히 사람의 검토가 필요하고, 암호 원시 요소 자체는 안전하다는 가정 위에 놓여 있다. Signal 사용자가 할 일은 아무것도 없다. 이것은 취약점 수정이 아니며 설치할 패치도 없다. Signal 측은 에이전트가 실제 코드를 자동으로 유효한 Lean 정리로 변환할 수 있게 된 것을 '중대한 돌파구'라고 평가했다.
형식 검증이 논문에서 엔지니어링으로 이동하고 있다. 마이크로소프트도 AI 에이전트 안전 연구를 추진하고 있다.마이크로소프트, Lazarus 백도어 발견: 10개 미만의 뉴런으로 에이전트 조종 가능에이전트가 유능해질수록 '해야 할 일만 한다'는 것을 검증하는 일은 더 중요해진다.
Signal에서 출발, 다음은 어디로
딥마인드의 다음 단계는 이 방법을 Signal에서 의료기기 펌웨어, 전력망 소프트웨어 같은 다른 핵심 시스템으로 확장하는 것이다. 증명을 써낸 것은 시작에 불과하다. 더 많은 시스템에서 재현할 수 있는지가 이것이 보안 업계의 새로운 기반이 될지를 결정한다.
