사람은 스펙을 보고, 기계는 코드를 본다

GitHub Next와 Microsoft Research가 10월 21일 Proof-Driven Development Kit을 발표했다. 연구 프리뷰이고, Rust에서만 돌아간다. 그리고 코딩 에이전트를 돌리는 대부분의 팀이 피해온 주장을 꺼낸다. 더 이상 diff를 한 줄씩 읽을 수 없다면, 읽을 수 있는 척은 그만두고 다른 걸 리뷰하라는 것이다.

그 '다른 것'이 스펙이다. PDD Kit의 워크플로에서는 사람이 스펙을 승인하고, 기계가 가능한 모든 입력에 대해 구현이 그 스펙을 만족하는지 검사한다.

다섯 단계, 그리고 사람이 앉는 자리

루프는 이렇게 돈다. 팀이 먼저 Chopin에서 기능을 계획한다. Chopin은 GitHub Next의 멀티플레이어 에이전트 기획 도구다. 그다음 PDD Kit이 코드를 두고 논의하고, 의도를 추론하고, Verus로 작성된 형식 스펙을 제안한다. Verus는 Rust를 위한 기존 오픈소스 증명 언어다. 사람이 승인하는 것은 스펙이지 코드가 아니다. 이어서 Verus가 에이전트가 생성한 코드가 모든 입력에서 그 스펙을 만족함을 증명한다. 완전한 증명이 불가능한 곳에서는 PDD Kit이 테스트와 computer-use 에이전트를 통한 경험적 확인으로 물러나고, 결과물은 검증된 pull request다.

이 뒤집기가 핵심 전부다. 사람은 요구사항을 리뷰한다. 검증기는 구현을 리뷰한다. Verus에서 스펙은 함수에 사전조건과 사후조건을 붙이고, 검증기가 그것을 discharge해야 한다. 보장은 특정한 의미에서 초록불 테스트 스위트보다 강하다. 테스트는 입력을 샘플링하고, 증명은 모든 입력에 대해 정량화한다.

GitHub의 설명은 이렇다. Chopin과 PDD Kit을 쓰면 AI가 만든 코드를 한 줄씩 리뷰하지 않고도 프로덕션에 내보낼 수 있고, 코드 리뷰와 테스트만으로 얻는 것보다 강한 보장을 얻는다. 다만 이건 벤더가 자기 연구 프리뷰를 설명하는 말이지 감사를 거친 결과가 아니다. 너무 꽉 쥐지 않는 게 좋다.

{{INLINE1}}

비용은 사라지지 않고 자리만 옮겼다

'리뷰 부담이 해결됐다'로 읽고 싶어진다. 아니다. 부담은 파이프라인 앞단으로 옮겨갔고, 과소평가하기 쉬운 방식으로 더 어려워졌다.

증명 가능할 만큼 정확한 스펙을 쓰는 것은 diff를 리뷰하는 것과 다른 기술이다. 모호한 요구사항은 증명 불가능한 스펙을 낳고, 검증기는 실패로 그 사실을 알려준다. 그래서 도입 첫 몇 주는 '안 되는 도구'처럼 보인다. 실제로 일어나는 일은 요구사항의 모호함이 평소보다 이른 시점에, 그럴듯한 함수로 덮어버리지 않는 무언가에 의해 드러나는 것이다.

아무도 읽지 않는 설계 문서를 계속 써온 팀에게 이건 실제 변화다. 설계 문서가 하중을 받는 부재가 된다. 검사받는 산출물이 그것이 되기 때문이다.

증명이 멈추는 곳

기능 목록보다 중요한 제약이 세 가지다.

Rust만. Verus가 검사하는 것은 Rust이고, GitHub Next는 PDD Kit이 현재 Rust에서 동작한다고 말한다. 새 언어도 없고, 코드가 만들어지는 방식의 변화도 없다. 에이전트가 TypeScript나 Python을 쓴다면 지금 설치할 것은 없다. 프로덕션 코드 중 얼마나 많은 부분이 Rust가 아닌지를 생각하면, 짧은 문장을 걸친 커다란 제약이다.

스펙이 표현할 수 있는 것만. 형식 증명은 정확히 서술할 수 있는 성질을 다룬다. 입출력 계약, 불변식, 상태 기계 전이. UI 동작, I/O가 많은 로직의 대부분, '올바름'이 성질이 아니라 판단인 것은 다루지 못한다. 그 전부는 테스트와 사람 리뷰라는 폴백 경로로 내려가고, 그곳이 바로 오늘의 부담이 이미 사는 자리다.

연구 프리뷰이고, 이력이 구체적이다. Chopin은 GitHub Next의 프로젝트 페이지에 2026년 9월자 연구 프로토타입으로 올라 있다. GitHub Next는 전에도 프로토타입을 내놓았다. Repo Mind, Project Copernicus, SpecLang 같은 것들이고, 일반 공개에는 이르지 못했다. 실제 코드를 대상으로 한 첫 공개 데모는 GitHub Universe, 10월 28~29일로 예정돼 있다.

정직함은 폴백 쪽에 있다

가장 많은 것을 말해주는 설계 결정은 증명기가 아니다. 증명할 수 없는 코드를 위한 두 번째 경로를 명시적으로 둔 것이다. 테스트와 computer-use 에이전트를 통한 경험적 확인으로 보내는 경로다.

대부분의 검증 도구가 하지 않으려는 인정이다. 증명 가능한 코드가 있고 아닌 코드가 있으며, 아닌 척하는 것이 파이프라인 두 개를 내놓는 것보다 나쁘다고 아키텍처 안에서 말한다. 이걸 쓰는 팀은 결국 모듈마다 라벨을 갖게 된다. 증명됨, 테스트됨, 리뷰됨. 커버리지 리포트가 만들어내는 어떤 숫자보다 정직한 신뢰도 재고다.

걸리는 건, 폴백 경로가 에이전트가 자기 숙제를 채점하는 자리이기도 하다는 점이다. UI를 클릭해 변경이 먹혔는지 확인하는 computer-use 에이전트도 여전히 에이전트고, 여전히 샘플링하며, 망가진 흐름을 '괜찮아 보인다'고 결론 내릴 수 있다. 증명 경로가 주는 것은 증명이다. 폴백이 주는 것은 통과해버린 데모다.

밑에 깔린 연구가 안심되는 부분

PDD Kit은 처음부터 만든 검증기가 아니다. Verus는 별개이고 이미 자리 잡혀 있다. Microsoft Research의 verus-proof-synthesis 저장소에 토대가 있다. LLM으로 돌아가는 두 시스템 AutoVerus와 VeruSAGE가 Verus 증명을 생성하고 수리하며, 각각 150개와 849개 검증 과제로 벤치마크됐다.

PDD Kit이 더하는 것으로 보이는 것은 포장이다. 이 증명 합성 연구 계보가 벤치마크 연습이 아니라 계획에서 PR까지 가는 제품 워크플로에 접힌 것은 처음이다. 'AI가 자기 코드를 증명할 수 있다'보다 작은 주장이고, 더 믿을 만한 주장이다.

이름이 소스마다 엇갈린다는 점도 짚어두자. 같은 주 보도에 Proof-Driven Development Kit과 Property-Driven Development Kit이 둘 다 나오고, 둘 다 같은 발표에 연결된다. 하나 골라서 넘어가면 된다. 어느 쪽이든 브랜딩을 하는 건 약어다.

오늘 할 수 있는 것

오래 남을 결론은 'GA를 기다려라'가 아니다. 에이전트가 많은 코드베이스는 이제 증명 가능한 영역과 아닌 영역으로 갈라지고, 설정은 이미 어느 쪽이 어느 쪽인지 알고 있어야 한다는 것이다.

파서, 상태 기계, 자료구조 불변식, 경계가 있는 산술, 동시성 프리미티브. 여기가 증명 가능한 영역이고, Verus는 오픈소스이며 지금 쓸 수 있다. PDD Kit이 있든 없든. 프런트엔드 작업 대부분, 글루 코드 대부분, 그리고 정확성이 '사용자가 무엇을 의도했는가'에 달린 것은 아니다.

실무적인 움직임 두 가지가 따라온다. 첫째, 저장소에서 증명 가능한 모듈에 태그를 달고 에이전트를 그쪽으로만 Verus에 겨누라. 벤더가 워크플로를 내놓기 전에. 둘째, 에이전트에게 자기 일을 검증하는 테스트까지 쓰게 하는 걸 그만두라. 그 배치는 늘 이해충돌이었고, 초록 스위트의 의미가 예전 같지 않은 이유다.

불편한 질문

스펙을 사람이 승인하고 증명을 기계가 discharge할 수 있다면, 리뷰어는 대체 뭘 하는 사람인가. 코드를 읽는 사람이 아니고, 아마 에이전트가 412번째 줄에 넣은 버그를 잡는 사람도 아니다.

리뷰어의 일은 원래 그래야 했던 것이 된다. 시스템이 무엇을 해야 하는지 정하고, 그걸 말하지 않은 스펙을 거부하는 것. diff에 승인을 누르는 것보다 어렵다. 그리고 검증기가 대신해줄 수 없는 유일한 부분이기도 하다.