MS 연구진, AI가 쓴 로그인 코드 수학으로 증명

마이크로소프트 리서치는 11월 5일(현지시간) AI 에이전트가 작성한 Rust 웹앱의 로그인 로직이 명세를 모든 입력에서 만족한다는 것을 연구 시제품 PDD Kit로 기계 검증했다고 밝혔다. 약 5,000줄 규모 앱의 일부를 검증한 사례로, 개발자는 생성된 코드를 한 줄씩 읽지 않고 의도만 검토했다.

핵심 정리

• PDD Kit는 개발자의 자연어 의도를 형식 명세로 바꾸고, 검증기 Verus로 에이전트가 쓴 Rust 코드를 명세와 대조한다.
• 예제 앱 Pet Store에서는 두 문장 요청이 증명 조항 8개가 됐고, 함수 5개를 증명했으며 6개 요소는 신뢰 대상으로 남겨 테스트했다.
• 현재는 Rust만 지원하는 연구 시제품이며, 발견한 버그 수와 증명 비용은 공개되지 않았다.

AI 코드 형식 검증, PDD Kit는 어떻게 작동하나

PDD Kit는 GitHub Next의 다중 사용자 계획 도구 Chopin 안에서 돌아간다. 계획 단계에서 코드를 읽고, 코드를 쓰기 전에 질문을 던진 뒤, 답변을 팀이 검토하는 문서로 정리한다. 이후 코딩 에이전트가 구현과 증명을 작성하면 Verus가 Z3 솔버로 결과를 확인한다.

마이크로소프트 리서치 블로그는 "리뷰는 '맞아 보이는가'를 묻고, 증명은 '맞는가'에 답한다"고 설명했다. 명세·코드·증명은 모델이 쓰지만 통과 여부는 결정론적인 Verus 실행이 가른다.

검사 시간은 작은 모듈이면 보통 몇 초, 큰 코드베이스는 몇 분까지 걸린다고 회사는 밝혔다. 이 검사를 CI에 넣으면 증명이 깨질 때 빌드가 실패한다.

Pet Store 로그인에서 증명한 것

개발자의 요청은 "올바른 비밀번호일 때만 토큰 발급", "관리자 계정만 관리자 토큰 발급" 두 가지였다. PDD Kit는 올바른 비밀번호면 반드시 통과해야 하는지 되물었다. 모두를 거부하는 로그인도 첫 규칙만은 지키기 때문이다.

이 과정을 거쳐 ensures 조항 8개와 작업 7개짜리 빌드 계획이 나왔고, 함수 5개가 모든 입력에 대해 증명됐다. 아무것도 걸러내지 못하는 빈 조항, 이른바 '바이브 검증'을 막기 위해 조항마다 버그를 하나씩 심은 복사본을 Verus가 거부하는지도 확인한다.

증명이 닿지 않는 곳

데이터베이스 조회 2건, bcrypt 비밀번호 검사, 토큰 서명, 시계, 데이터베이스 오류 메시지, 핸들러의 요청 해석 등 6개 요소는 증명 밖에 있다. 개발자가 하나씩 승인했고 테스트로 확인했다.

연구진은 "보장은 신뢰하는 6개 요소만큼만 강하다"고 적었다. 로그인이 끝난다는 점이나 시도 빈도·응답 시간도 약속하지 않는다. 기존 버그를 찾았다고 했지만 목록은 밝히지 않았고, AI Newsway는 독립 평가를 찾지 못했다.

형식 검증이 다시 주목받는 이유

에이전트가 만드는 코드량이 사람의 리뷰 능력을 넘어서면서 증명이 대안으로 떠오르고 있다. AI가 만든 보안 패치가 다른 기능을 깨뜨린다는 Trail of Bits의 재검증 결과도 같은 문제의식이다. Anthropic은 10월 22일 Claude로 오픈소스 라이브러리 123개의 무충돌을 증명했다고 밝혔다. AlphaSignal에 따르면 PDD Kit는 10월 21일 연구 프리뷰로 처음 소개됐다.

전망

마이크로소프트는 로그인·결제·권한처럼 버그 비용이 큰 곳부터 적용하라고 권했다. 신뢰 경계는 줄어들 것으로 내다봤고, 어디까지 확장되는지 확인하겠다고 했다.

자주 묻는 질문

증명되면 버그가 없는 코드인가? 아니다. 명시한 가정 아래 코드가 명세를 만족한다는 뜻이며, 명세 자체가 틀릴 수 있다.

다른 언어에서도 쓸 수 있나? 직접은 어렵다. Rust로 옮기거나 바인딩으로 검증된 Rust를 호출해야 한다.

참고 자료

• Formally verifying agent-written full-stack web apps with PDD Kit — Microsoft Research(2026.11.5)
• GitHub - verus-lang/verus: Verified Rust for low-level systems code — Verus 프로젝트
• Chopin — GitHub Next
• Microsoft's PDD Kit Makes Formal Math Proofs a Gate for AI Rust Code — AlphaSignal(2026.10.21)