PDD Kit, Verus로 에이전트가 작성한 풀스택 웹 앱의 로그인 로직 형식 검증

Formally verifying agent-written full-stack web apps with PDD Kit

Microsoft Research가 AI 코딩 에이전트가 작성한 코드를 Verus 기반 형식 증명으로 검증하는 도구 PDD Kit을 공개했다. 개발자가 의도를 형식 명세로 옮기면 에이전트 코드가 모든 입력에 대해 명세를 충족하는지 증명하고, 증명이 닿지 않는 부분은 테스트로 보완한다. PDD Kit은 GitHub Next의 실시간 협업 기획 환경 Chopin 안에서 동작하며, 팀이 평이한 언어로 의도를 검토하면 도구가 이를 intent artifact라는 문서에 기록하고 형식 명세와 비형식 테스트 명세로 나눈다. 형식화 가능한 부분은 Rust용 증명 언어 Verus로 명세화되어 코드가 모든 입력에 대해 명세를 충족한다는 증명이 자동 생성되며, 테스트로 다뤄야 하는 부분은 단위·E2E 테스트, 터미널 자동화, 브라우저 에이전트, 컴퓨터 사용 에이전트로 검증한다. 시연에서는 Rust로 작성된 Pet Store 스토어프런트의 로그인 로직을 대상으로 적용했고, 개발자는 생성된 코드를 한 줄씩 읽지 않고 의도만 검토했다. Verus가 코드를 강화하면서 기존 버그도 찾아냈고, 명세 기준으로 로그인 버그가 없음을 증명했다고 기사는 밝혔다. 증명과 테스트의 경계는 신뢰 컴퓨팅 기반(TCB)으로 정의되며, 증명이 전제하는 코드가 명세대로 동작한다는 가정을 PDD Kit이 명시적으로 드러내 각 부분마다 개발자의 승인을 받도록 한다. 테스트로 검증된 항목은 증명이 아니라 증거로 분류되며, 제3자 암호화 라이브러리나 사용자 인터페이스처럼 증명이 닿지 않는 영역은 이 방식에 해당한다고 기사는 설명한다.