GitHub의 PDD kit: AI가 짠 코드의 정확성을 증명하기

AI 코딩 에이전트가 한 줄 요청으로 코드를 대량 생성하면서 생기는 검증 공백을 다룹니다. GitHub의 Spec kit은 명세와 계획을 먼저 쓰도록 구조화하고, PDD kit은 명세를 형식 논리로 만들어 증명까지 하려는 도구라는 차이를 비교합니다.

⏱ 00:00AI 코딩 에이전트에 짧은 요청을 입력하면 몇 초 만에 수백 줄의 코드가 나오지만, 비밀번호 규칙이나 잠금 조건처럼 세부 동작이 어떻게 정해졌는지는 알기 어렵습니다. 에이전트가 추측한 내용을 사람이 확인하려면 결국 모든 줄을 읽어야 하고, 이것이 검토의 병목이 됩니다.

요구사항은 시간이 지나며 흐려지고 문서는 낡아, 나중에는 코드 자체가 시스템이 무엇을 해야 하는지에 대한 유일한 기록이 됩니다. 발표는 이 문제를 해결하려면 코드를 짜기 전에 의도를 먼저 적고, 코드가 그 의도에 맞도록 만들어야 한다는 출발점에서 시작합니다.

⏱ 01:02Spec kit은 GitHub가 공개한 명세 주도 개발용 오픈소스 도구로, MIT 라이선스로 무료 제공되며 GitHub에서 인기 있는 AI 개발 도구 중 하나입니다. 자체가 코딩 에이전트를 대체하지 않고, Copilot, Claude, Gemini, Codex 같은 기존 에이전트에 붙어 구조화된 작업 절차를 제공합니다.

핵심 루프는 명세, 계획, 작업 분해, 구현, 수렴의 다섯 단계입니다. 그 위에는 프로젝트의 원칙을 한 번 적어 두는 헌법이 놓여, 이후 모든 단계가 이 규칙에 비추어 검토됩니다. 시작하려면 Python 3.11 이상과 UV 도구, 지원되는 에이전트가 필요하며 Linux, Mac, Windows에서 모두 동작합니다.

⏱ 02:02먼저 헌법 단계에서 모든 기능에 테스트가 있어야 하고, 비밀번호는 평문으로 저장하지 않으며, 보안 규칙은 백엔드에 둔다는 식의 협상 불가 원칙을 적습니다. 명세 단계에서는 기술 이름 없이 사용자가 무엇을 원하고 왜 필요한지를 설명하면, 도구가 사용자 스토리와 번호가 붙은 요구사항, 성공 기준을 담은 명세 문서를 만듭니다.

명세에 특정 기술 이름이 끼어들면 계획 단계로 옮기라는 것이 발표의 요령입니다. 선택 사항인 명확화 단계에서는 에이전트가 모호한 부분을 질문하고, 답변을 명세에 반영합니다. 계획 단계에서 기술 스택과 데이터 모델, API 계약을 정하고, 작업 단계에서는 계획을 사용자 스토리별 번호 목록으로 쪼개며 각 작업이 건드릴 파일과 병렬 실행 가능 여부를 표시합니다. 분석 단계는 명세, 계획, 작업을 함께 읽어 모순이나 빈틈을 보고하되 코드는 바꾸지 않습니다.

⏱ 03:52구현 단계에서는 에이전트가 작업을 순서대로 처리하며 코드를 작성합니다. 수렴 단계에서는 완성된 코드를 합의된 명세와 대조하고, 빠진 부분이 있으면 코드를 직접 고치지 않고 새 작업을 추가합니다. 수렴이라고 판정될 때까지 구현과 수렴을 반복하는 구조입니다.

Spec kit은 신규 기능 외에도 확장 기능으로 영역을 넓힙니다. 버그 확장은 원인 진단, 수정, 검증을 분리해 실제 원인을 고쳤는지, 원래 증상이 사라졌는지 확인하게 합니다. 평가 확장은 아이디어를 만들기 전에 조사해 진행, 명확화 필요, 중단 중 하나의 결론을 내립니다. 프리셋, 워크플로, 번들로 팀의 기준에 맞춰 조정할 수 있지만, 커뮤니티 확장은 검증되지 않았으니 설치 전에 소스를 읽어야 한다고 강조합니다.

⏱ 04:51PDD kit은 proof-driven development kit의 약자로, GitHub Next와 Microsoft Research에서 나왔으며 현재는 연구 미리보기 단계입니다. 지금은 Rust에서만 동작하고, Rust용 오픈소스 증명 언어인 Verus를 사용합니다. 질문의 방향이 다릅니다. 테스트로 몇 가지 경우를 확인하는 대신, 모든 가능한 입력에 대해 코드가 명세를 만족하는지를 증명하려 합니다.

흐름은 팀이 함께 계획을 세우고, 도구가 코드를 읽어 의도를 형식 명세로 제안하면, 사람은 코드가 아니라 명세를 승인하는 순서입니다. 로그인 예시에서는 실패 횟수가 5회 미만일 때만 로그인을 허용한다는 한 줄짜리 명세가 만들어집니다. Verus 검증기가 모든 입력에 대해 증명하며, 허용 횟수를 하나 잘못 두면 증명이 바로 실패해 배포 전에 걸러집니다. 증명할 수 없는 로그인 화면 같은 부분은 테스트와 화면을 조작하는 에이전트로 보완합니다.

⏱ 06:21Spec kit의 명세는 사람과 에이전트가 읽는 마크다운이고, PDD kit의 명세는 기계가 검사할 수 있는 형식 논리입니다. Spec kit은 어떤 언어와 여러 에이전트에서 쓸 수 있지만, PDD kit은 현재 Rust에만 적용됩니다. 검증 방식도 Spec kit은 테스트와 수렴 단계에 의존하고, PDD kit은 증명에 의존합니다.

둘은 경쟁 관계라기보다 역할이 다릅니다. Spec kit은 작업 전체의 구조를 잡고, PDD kit은 버그가 생기면 가장 큰 피해가 나는 부분을 증명합니다. 다만 명세 자체가 틀리면 잘못된 것이 명세대로 정확히 만들어진다는 공통된 한계가 있습니다. 규칙, 파서, 상태 기계에는 증명이 잘 맞고, 사용자 인터페이스나 입출력이 복잡한 부분은 여전히 테스트와 사람의 확인이 필요합니다. 웹 앱이라면 Spec kit으로 시작하고, 버그 비용이 큰 Rust 코드라면 PDD kit의 출시를 지켜볼 만합니다.