AI가 코드를 만드는 시대는 지났다. 이제 그 코드가 안전하다는 것까지 증명한다
구글 딥마인드가 AI와 인간 전문가의 협업으로 Signal 암호화 코드의 핵심 보안 속성을 수학적으로 증명했다. AI 코딩 경쟁의 다음 승부는 얼마나 빨리 만드느냐가 아니라, 얼마나 확실하게 검증하느냐에 있을지 모른다.
20초 핵심
1. AI가 만든 코드, 정말 믿어도 될까?
AI에게 프로그램을 만들어 달라고 하면 순식간에 코드가 나온다. 하지만 은행의 송금 시스템이나 병원의 의료기기라면 이야기가 달라진다. 중요한 것은 코드가 얼마나 빨리 만들어졌느냐가 아니다. 실수하면 안 되는 상황에서 정말 올바르게 작동하느냐다.
구글 딥마인드가 발표한 AlphaProof Code는 이 질문에 새로운 답을 내놓았다. Gemini 기반 AI 에이전트와 인간 전문가가 협력해, Signal 암호화 프로토콜의 실제 구현 코드가 핵심 보안 조건을 지킨다는 것을 수학적으로 증명했다.
AI 코딩의 다음 단계는 더 많은 코드를 만드는 일이 아니라, 그 코드를 믿을 근거를 만드는 일이다.
2. 테스트와 증명은 무엇이 다를까?
다리를 만들었다고 생각해 보자. 트럭 몇 대를 실제로 지나가게 하면서 문제가 없는지 살펴보는 것이 일반적인 테스트에 가깝다. 반면 정형검증(Formal Verification)은 설계와 조건을 수학적으로 표현하고, 정해진 조건 안에서 구조가 요구사항을 만족한다는 사실을 논리적으로 입증하는 과정에 가깝다.
실제로 달려본다
여러 상황을 실행해 오류를 찾는다. 시험하지 않은 상황은 남는다.
수학적으로 따져본다
지켜야 할 조건을 명시하고, 코드가 그 조건을 충족함을 증명한다.
이번 성과가 특히 흥미로운 이유는 추상적인 설계도가 아니라 실제 사용되는 암호화 코드의 구현 수준을 검증했다는 점이다. 설계는 완벽해도 프로그램으로 옮기는 과정에서 실수가 생길 수 있기 때문이다.
테스트가 오류를 찾아내는 방식이라면, 정형검증은 명시한 보안 조건이 성립한다는 근거를 쌓는 방식이다.
3. 4주 동안 무엇을 확인했나?
이번 작업에서 AI와 전문가들은 방대한 증명 코드를 만들어 Signal의 핵심 보안 속성을 검토했다. 증명 코드만 300만 줄 이상이고, 작업에는 약 4주가 걸렸다.
검증 능력을 확인하는 실험도 진행했다. 과거에 발견돼 이미 고쳐진 취약점 두 개를 코드에 일부러 다시 넣었다. AlphaProof Code는 두 경우 모두 문제를 찾아냈다. AI가 그럴듯한 설명만 만든 것이 아니라, 잘못된 구현을 구별하는 데 실제로 활용될 수 있음을 보여준 사례다.
물론 정형검증은 처음부터 정의하지 않은 위험이나 잘못 세운 가정까지 자동으로 해결하지는 못한다.
AI가 만들어낸 답을 다른 수학적 검증 체계로 확인하는 방식이 소프트웨어 신뢰성의 문턱을 낮추기 시작했다.
4. 기업은 왜 '더 빠른 코딩'보다 '더 확실한 코드'에 돈을 낼까?
코드를 작성하는 비용이 낮아질수록 기업들이 더 비싸게 평가할 일은 달라진다. 금융에서는 잘못된 거래가, 의료에서는 기기의 오작동이, 통신과 보안에서는 정보 유출이 큰 비용으로 이어진다. 이런 산업에서는 코드를 한 시간 먼저 만드는 것보다 반드시 지켜야 할 규칙을 증명하는 능력이 더 중요할 수 있다.
개발자의 역할도 바뀐다. AI에게 코드를 시키는 사람에서, 시스템이 반드시 지켜야 할 조건을 정의하고 AI가 내놓은 증명을 검토하는 사람으로 무게중심이 옮겨갈 수 있다.
Alphabet(GOOGL) 투자자에게는 Gemini의 활용 영역이 개발 생산성을 넘어 고부가가치 엔지니어링 검증으로 확장될 수 있다는 점이 중요하다. AI 코딩 서비스의 경쟁 기준이 작성 속도에서 신뢰성까지 넓어지는 것이다.
코드가 흔해질수록 기업이 돈을 지불할 이유는 '생산량'보다 '실수를 줄이는 확실성'에서 커진다.
5. 투자자가 다음으로 확인할 신호
- 제품화 : 구글이 이 기술을 클라우드 또는 개발도구에 통합하는지. 연구 성과가 실제 고객의 작업 흐름으로 들어가는 첫 관문이다.
- 고객 도입 : 금융회사나 보안 기업이 실제 업무에서 정형검증을 사용하는 사례가 나오는지. 기술적 성공이 경제적 가치로 연결되는지 보여준다.
- 경쟁사의 대응 : 마이크로소프트와 OpenAI 등이 코드 검증 기능을 강화하는지. AI 코딩 경쟁의 평가 기준이 바뀌고 있는지 확인할 수 있다.
AI가 코드를 쓰는 속도는 이미 놀랍다. 앞으로 더 중요한 질문은 따로 있다. 누가 그 코드의 올바름을 가장 설득력 있게 증명할 수 있는가?
투자 관점에서 보면 중요한 변화가 보인다. AI의 경제적 가치가 코드를 만드는 단계에서, 만들어진 코드의 신뢰성을 확보하는 단계로 확장되고 있다.
AI가 작성한 코드가 늘어날수록 검증해야 할 코드도 늘어난다. 이 시장에서는 모델의 코딩 실력뿐 아니라 개발도구와 클라우드에 검증 기능을 얼마나 자연스럽게 연결하는지가 경쟁력이 될 것이다.
- 구글 딥마인드가 발표한 코드 검증용 AI 시스템이다.
- Gemini 기반 AI 에이전트가 인간 전문가와 함께 Signal 암호화 프로토콜의 구현 코드를 수학적으로 증명했다.
- 테스트는 여러 상황을 실제로 실행해 오류를 찾는 방식이다. 시험하지 않은 상황은 남는다.
- 정형검증은 지켜야 할 조건을 적고 코드가 그 조건을 만족한다는 것을 수학적으로 따지는 방식이다.
- 작업에는 약 4주가 걸렸다.
- 생성된 증명 코드는 300만 줄 이상이다.
- 그렇게 보기는 어렵다. 정형검증은 처음에 정의하지 않은 위험이나 잘못 세운 가정까지 자동으로 해결하지 못한다.
- 명시한 보안 조건이 성립한다는 근거를 쌓는 일로 보는 편이 맞다.
- 과거에 발견돼 이미 고쳐진 취약점 두 개를 일부러 다시 넣는 실험을 했다.
- AlphaProof Code는 두 경우 모두 문제를 찾아냈다.
체크 포인트
인사이트 타임스 편집부
