Microsoft Research, PDD Kit 공개 에이전트 코드를 Verus로 증명

Microsoft Research가 코딩 에이전트가 작성한 코드를 수학적으로 증명하는 도구 모음 PDD Kit와 그 적용 사례를 11월 5일(현지시간) 블로그에 공개했다. 사용자의 의도를 형식 명세로 바꾸고, 에이전트가 짠 코드가 그 명세를 모든 입력에서 만족하는지 증명하며, 증명이 닿지 않는 부분은 테스트로 확인하는 방식이다.

PDD Kit는 연구 프로토타입이며, 지금은 Rust 코드만 검증한다. 검증기로 쓰는 Verus가 Rust용이기 때문이다. 다른 언어 코드는 Rust로 옮겨 같은 명세로 검증할 수 있고, Rust가 아닌 프로젝트는 바인딩으로 검증된 Rust 코드를 호출할 수 있다고 연구팀은 설명했다. 요금과 배포 방식은 글에 나오지 않는다. 필자는 Alex Lavaee와 Matthai Philipose다.

계획과 테스트만으로 모자라는 이유

코딩 에이전트는 이제 수만~수십만 줄에 이르는 기능을 한 번에 내놓기도 하며, 연구팀은 이런 규모에서는 풀 리퀘스트를 전부 한 줄씩 읽는 검토가 따라가기 어렵다고 설명했다. 그래서 많은 팀이 에이전트에게 원하는 바를 설명하고 계획과 테스트를 맞춘 뒤 구현을 맡기는데, 계획이 계약 역할을 해야 하지만 에이전트가 계획에서 벗어나도 막을 장치가 없다고 지적했다. 에이전트는 약간 다른 것을 구현하고 그 구현에 맞는 테스트를 쓰기 때문에, 요청한 것과 배포된 것의 차이가 버그 보고가 나올 때까지 드러나지 않는다는 설명이다.

에이전트 코드는 꼭 필요한 것을 빼먹거나 명백히 잘못된 일을 하는 두 가지로 실패하는데, 테스트는 프로그램이 할 수 있는 동작의 일부만 실행하므로 이 틈을 메우지 못한다고 연구팀은 밝혔다. 검토는 "이게 맞아 보이는가"를 묻고 증명은 "이게 맞는가"에 답한다는 것이다. 예전에는 전문가, 낯선 언어, 코드보다 훨씬 긴 증명, 수년의 시간이 필요해 일반 소프트웨어에 쓰기 어려웠지만, 에이전트가 명세와 증명 작성을 돕게 되면서 사정이 달라졌다고 연구팀은 주장했다. 이 개발 방식을 증명 주도 개발(Proof-Driven Development, PDD)이라 부른다.

작동 방식

PDD Kit는 Spec Kit이 명세 주도 개발에서 맡는 역할을 형식 검증에서 맡는다. GitHub Next의 실시간 다중 사용자 계획 환경 Chopin 안에서 동작해, 팀과 에이전트가 하나의 문서에서 계획을 세운다. 팀원은 먼저 평이한 말로 의도를 검토한다. PDD Kit가 꼼꼼한 검토자가 던질 질문을 하고 관련 코드를 설명하면, 답은 의도 문서에 기록된다. 의도 중 형식화할 수 있는 부분은 형식 명세로, 나머지는 테스트용 비형식 명세로 바뀐다. 이후 코드가 형식 명세를 만족한다는 증명과 비형식 명세용 테스트가 자동 생성된다. 형식 검증 지식은 필요 없다고 연구팀은 밝혔다.

결과에는 어떤 검증에 기댄 것인지가 표시된다. 형식 검증은 검증기가 모든 가능한 입력에서 코드가 명세를 만족함을 수학적으로 확인하는 것이다. 지금 검증기는 Verus이고, Microsoft Research, Carnegie Mellon University, VMware Research, ETH Zurich 등 여러 기관이 함께 개발한 Rust용 증명 언어다. 경험적 검증은 코드를 실행해 동작을 관찰하는 방식이다. 서드파티 암호 라이브러리나 사용자 인터페이스처럼 증명이 닿지 않는 곳에 쓰며, 단위·종단 테스트, 터미널 자동화, 브라우저 에이전트, 컴퓨터 사용 에이전트를 동원한다. 통과한 테스트는 입력 몇 개에서 동작했다는 증거일 뿐이어서 PDD Kit는 증명이 아닌 증거로 표시한다.

두 방식의 경계는 증명이 설명대로 동작한다고 가정하는 코드, 곧 신뢰 컴퓨팅 기반(TCB)이다. PDD Kit는 이 경계를 명시하고 조각마다 개발자의 승인을 요구한다.

Pet Store 로그인 사례

시연 대상은 Rust로만 짠 풀스택 웹앱 Pet Store다. 백엔드는 Axum과 SQLite로 재고, 프로모션, 주문, 결제를 처리하고, 프런트는 WebAssembly로 컴파일한 Leptos 앱이다. 합쳐서 약 5,000줄이다. 글에서는 로그인 로직만 검증했다. 로그인 버그는 고객이나 관리자 계정을 공격자에게 넘길 수 있어 증명 노력이 가장 먼저 보상받는 곳이라는 이유다. 연구팀은 민감한 부분부터 점차 넓혀 가라고 권했다. Verus가 코드를 단단하게 만들고 기존 버그도 찾아냈으며, 명세 기준으로 로그인 버그가 없음을 증명했다고 밝혔다. 개발자는 의도만 검토하고 생성된 코드를 한 줄씩 읽지 않았다.

개발자가 Chopin에 낸 요청은 두 문장이었다. 백엔드 auth.rs의 로그인 로직을 검증하되, 올바른 비밀번호로만 토큰을 받고 관리자 계정만 관리자 토큰을 받는다는 요구였다. 요청은 일부러 거칠게 썼고, 의도를 증명이 확인할 수 있는 형태로 바꾸는 것이 PDD Kit의 몫이라고 연구팀은 설명했다.

계획 단계의 pdd-plan은 코드를 읽고 쓰기 전에 Decisions 탭에서 질문을 던진다. 첫 질문은 "올바른 비밀번호로만 토큰을 받는다"가 모두를 거부하는 로그인으로도 충족된다는 점이었다. 이 문장은 토큰이면 올바른 비밀번호라는 한 방향의 함의이고, 올바른 비밀번호면 항상 토큰을 받는다는 역방향을 더해야 "필요충분"이 된다. 방치된 에이전트라면 말없이 한쪽을 골랐겠지만 여기서는 개발자가 양방향을 선택했다. 계획 상단에는 흐름도, 증명할 것과 신뢰할 것을 보여 주는 명세 지도, 필요하면 비유 그림이 갱신되며, 의도 지도는 각 요구를 개발자 표현, 형식 명세 구간, 커버하는 테스트와 연결한다.

착수 전 팀은 계획 전체를 승인한다. PDD Kit의 첫 초안은 테이블 선택과 비밀번호 확인 판단만 증명하고 이를 감싼 핸들러는 신뢰하며 테스트하는 구성이었고, PDD Kit도 이를 권장했다. 개발자는 조회를 기다리고 토큰을 서명하는 연결 코드에서 리팩터링 때 두 줄이 바뀔 수 있다며, 로그인 핸들러에도 비동기 명세를 주어 증명 범위에 넣었다. 그 결과 요청 필드에서 토큰 또는 HTTP 오류까지의 계약을 담은 login_flow 함수가 생겼고, PDD Kit는 신뢰 범위가 바뀌었으므로 계획을 다시 승인받았다.

증명이 멈추는 곳과 명세

로그인에서 증명이 닿지 않는 것은 다섯 가지다. bcrypt 해싱, sqlx 쿼리, jsonwebtoken 서명처럼 다른 크레이트에 있는 코드, SQLite의 현재 내용과 시계 같은 외부 사실, 작업이 끝나는지와 속도, 오류 메시지나 화면이 쓸 만한지 같은 사람의 판단, 아무도 적지 않은 요구다. PDD Kit는 신뢰 경계의 조각마다 가정 계약을 두고 개발자에게 하나씩 수락받으며, 가정한 조항마다 테스트를 계획에 적는다. 개발자는 여섯 조각을 승인했다. 두 조회 함수(Customer::find_by_email, Admin::find_by_username), bcrypt::verify를 감싼 check_password, 서명 함수 generate_token, 24시간 뒤 만료를 계산하는 expiry_from_now, 조회 실패를 500으로 바꾸는 database_error다. 핸들러 껍데기는 요청을 풀어 login_flow에 넘기는 일만 한다. 계획은 로그인 future가 끝난다는 점, 범위를 벗어난 시계가 패닉을 내지 않는다는 점, 시도 횟수와 속도, 다른 엔드포인트가 역할을 읽는 방식은 아무도 약속하지 않는다고 적었다.

팀이 검토하는 의도 문서는 Verus 계약의 평이한 버전이다. 코딩 에이전트가 증명을 쓰고 Verus가 모든 단계를 검사하므로 증명을 읽는 사람은 없다. 각 함수의 ensures 블록은 모든 입력에서 성립해야 하는 결과 조건이며, 한 입력이라도 어기면 빌드가 실패한다. login_flow에는 두 문장 요청과 양방향 결정이 여덟 개의 ensures 조항으로 정리됐고, 그중 넷은 기존의 거부 동작을 유지해 프런트와 기존 API 테스트가 계속 동작한다. 한 조항은 비밀번호 확인과 토큰이 같은 계정을 가리키게 묶는다. 밥이 자기 비밀번호로 로그인했는데 앨리스 계정의 토큰이 나가는 배선 버그를 잡는 장치로, 테스트가 좀처럼 떠올리지 못하는 유형이라고 연구팀은 설명했다.

login_flow는 비동기 함수라 데이터베이스 조회를 기다린다. Verus는 비동기 함수에도 계약을 줄 수 있는데, requires는 future를 만들 때, ensures는 기다려 얻은 값에 대해 검사된다. future가 끝난다는 약속은 없어서 멈춘 쿼리가 조항을 깨지 않는다. 함수는 lookup_target, login_core, decide_login, issue_token 같은 작은 증명 조각으로 나뉘고, Verus는 각 계약만으로 login_flow를 증명하므로 한 조각의 본문이 바뀌면 그 조각만 다시 증명한다.

증명, 병합, 한계

개발자가 명세를 승인하면 사람의 검토는 끝나고 나머지는 기계가 검사한다. 그 전에 검토 에이전트 둘이 의도 문서에서 파생된 명세의 허점을 찾는다. 이어 pdd-prove가 로그인을 일곱 개 작업으로 쪼갠다. login.rs를 Verus로 빌드하는 작업, 판단·토큰·전체 흐름 증명, 신뢰 래퍼와 종단 로그인 테스트 작성이다. 작업마다 코딩 에이전트가 구현과 증명을 쓰고 Verus가 검사하며, 신뢰 경계에는 계획된 테스트가 붙는다. LLM 검증기가 계획, 명세, 결과를 나란히 읽어 증명도 통과 검사도 없는 요구를 찾고, 명세 자체에 모순이 있으면 개발자에게 결정으로 돌려보낸다. 비동기 구문을 표현할 수 없으면 계약을 약화하거나 우회하지 않고 멈춰서 팀에게 묻는다.

연구팀은 모델이 스스로 명세를 쓰거나 증명용으로 조정되면 검증은 통과하지만 거의 아무것도 배제하지 않는 약한 조항에 머물기 쉽다며, 이를 "vibe verification"이라 불렀다. 이를 막으려고 pdd-prove는 ensures 조항마다 버그를 하나씩 심은 복사본(모두 거부하기, 이메일보다 사용자명 먼저 확인하기 등)을 만들고, Verus가 해당 조항에서 각각 거부해야 한다. 통과하는 변이체가 있으면 그 조항이 아무 제약도 하지 않는다는 뜻이어서 공백으로 돌아온다.

작업이 통과하면 풀 리퀘스트가 열린다. verified/ 크레이트에 login_flow와 증명, 신뢰 래퍼와 테스트가 들어가고 실제 로그인 핸들러가 login_flow를 거치도록 바뀌며 기존 HTTP 상태 코드는 유지된다. 설명란에는 각 요구가 형식 검증인지 경험적 검증인지 표시돼 영수증 역할을 한다. 개발자는 생성 코드를 줄 단위로 검토하지 않고 병합했다. pdd-ship은 Verus 검사를 CI에 테스트와 나란히 넣어, 이후 사람이나 에이전트의 모든 변경이 같은 명세에 대해 증명돼야 하고 깨진 증명은 실패한 테스트처럼 빌드를 막는다. 이미 증명된 내용을 다시 확인하는 예시 기반 테스트는 정리하고 신뢰 경계를 지키는 테스트는 남긴다.

증명 범위는 login_flow, login_core, lookup_target, decide_login, issue_token의 본문이다. 올바른 테이블을 고르고, 요청 비밀번호를 지목된 계정의 저장 해시와 비교하며, 그 계정의 id와 테이블의 역할이 담긴 토큰을 내고, 나머지는 기존 400·401·500으로 거부한다는 것이다. 두 조회, bcrypt 기반 check_password, 시계, 토큰 서명, 데이터베이스 오류 메시지, 핸들러의 요청 풀기는 증명 밖에서 개발자가 수락한 계약에 기대며, 실제 bcrypt·SQLite 스키마·라우터를 상대로 한 테스트가 다룬다. Verus, Rust 컴파일러, Z3, 표준 라이브러리 vstd는 가정으로 남는다.

연구팀은 약한 고리도 직접 짚었다. 보장은 여섯 신뢰 조각만큼만 강하고, 비밀번호 약속 전체가 걸린 check_password와 어떤 계정의 토큰인지에 걸린 두 조회가 가장 무겁다. 이들은 테스트가 받칠 뿐 증명되지 않았고, 신뢰 경계가 시간이 갈수록 크게 줄 것으로 연구팀은 기대했다. 증명에는 여전히 노력이 들며 대부분 증명 작성에 쓰이고, 명세가 명확할수록 줄어든다. 연구팀은 로그인, 결제, 권한처럼 버그 비용이 큰 곳에서 시작해 한 조각씩 넓히라고 권했다. 명세가 의도와 다를 가능성도 남는데, 증명은 코드가 명세를 따른다는 것만 보이기 때문이다. 연구팀은 질문, 검토 에이전트 둘, 변이 검사, 개발자의 명세 승인으로 이를 줄인다고 밝혔다.

검증은 Z3 솔버를 쓰는 Verus의 결정적 실행으로, 모델은 개입하지 않는다. 모델은 명세, 코드, 증명을 쓰지만 통과 여부는 Verus가 정한다. 소요 시간은 작은 모듈이면 수 초, 큰 코드베이스면 수 분까지 걸린다. Verus를 고른 이유는 Rust를 직접 검증하기 때문이며, Lean, F*, Rocq 같은 다른 증명 언어도 각기 다른 장단점이 있다고 연구팀은 밝혔다. 이번 연구는 Microsoft Research Catalyst Lab, GitHub Next, RiSE 그룹의 협업이다.