2026년 11월 8일

AI가 짠 수만 줄의 코드, 어떻게 믿을까? Microsoft PDD Kit과 수학적 형식 검증(Formal Verification)

software-engineeringformal-verificationmicrosoft-researchpdd-kitrustveruscoding-agents

안녕하세요! 재니미입니다.

“코드 리뷰는 ’이 코드가 그럴싸해 보이는가(Does this look right?)’를 묻지만, 수학적 증명은 ’이 코드가 정말로 맞는가(Is this right?)’를 답합니다.”

2026년 11월 5일, Microsoft Research와 GitHub Next 연구진이 에이전트가 작성한 풀스택 웹 애플리케이션의 형식 검증 도구인 **PDD Kit(Proof-Driven Development Kit)**을 공개하며 기술 블로그 첫머리에 던진 질문입니다.

Claude Code, Cursor, Devin 같은 자율 코딩 에이전트가 개발 일상에 깊숙이 들어오면서, 이제 에이전트는 프롬프트 몇 줄만으로 수천 줄에서 수만 줄에 달하는 거대한 PR(Pull Request)을 순식간에 만들어냅니다.

결론부터 말씀드리면, 에이전트가 생성한 수만 줄의 코드를 인간이 눈으로 일일이 리뷰하거나, 에이전트가 자기가 짠 코드에 맞춰 작성한 단위 테스트에 의존하는 방식은 머지않아 한계에 부딪힐 수밖에 없습니다. 앞으로 엔지니어는 라인 바이 라인 코드 리뷰 노동에서 벗어나, 자연어 기획을 모호함 없는 정형 명세로 변환하고, Z3 SMT 솔버 기반의 Verus 증명기를 통해 가능한 모든 입력 공간에서 버그가 없음을 수학적으로 입증하는 PDD(Proof-Driven Development, 증명 주도 개발) 체계로 전환해야 합니다.

소프트웨어 공학의 거대한 패러다임 전환을 예고한 Microsoft PDD Kit의 구조와 실전 적용 사례를 알기 쉽게 정리해 드립니다.

1. 문제의 본질: 에이전트와 단위 테스트의 ‘공모’

현재 많은 개발 팀이 코딩 에이전트를 활용하는 워크플로는 대략 다음과 같습니다:

에이전트에게 자연어로 만들고자 하는 기능과 작업 계획(Plan)을 전달합니다.
에이전트가 비즈니스 로직을 구현하고, 그에 맞는 단위 테스트 코드까지 함께 작성합니다.
CI 파이프라인에서 테스트가 모두 초록색(Pass)으로 통과하면, 개발자는 변경 사항을 훑어본 뒤 머지합니다.

flowchart TD
    subgraph Trap ["현재 코딩 에이전트의 자기충족적 테스트 함정"]
        direction TB
        A["1. 인간: 자연어 요구사항 및 기획 전달"] --> B["2. 에이전트: 수만 줄의 비즈니스 코드 작성"]
        B --> C["3. 에이전트: 자기가 짠 로직에 맞춘 테스트 작성"]
        C --> D["4. CI 테스트 통과 (테스트 커버리지 100% 달성)"]
        D --> E["5. 프로덕션 배포 ➔ 예상치 못한 엣지 케이스 버그 폭발"]
    end

겉보기에는 완벽한 자동화처럼 보이지만, 여기에는 두 가지 치명적인 구조적 결함이 숨어 있습니다.

① 의도의 미묘한 이탈 (Plan Drift)

자연어 프롬프트는 엄밀한 수학적 구속력이 없습니다. 에이전트는 기획 의도와 미묘하게 다르게 코드를 짜놓고도, 자신이 잘못 구현한 동작을 그대로 통과시키는 테스트 코드를 아주 그럴듯하게 작성해 냅니다. 테스트 커버리지가 100%인데도 실제 서비스에 올리자마자 엉뚱한 결제가 일어나거나 권한 우회가 발생하는 이유입니다.

② 샘플링의 불완전성

단위 테스트는 무한대에 가까운 입력 공간 중 개발자나 에이전트가 상상해 낸 극히 일부의 샘플 케이스만을 실행해 볼 뿐입니다. 복잡한 멀티스레드 동시성 이슈나 경계 조건(Boundary Conditions)은 테스트 케이스 사이의 빈틈에 숨어 있다가 운영 환경에서 터져 나옵니다.

2. 해결책: PDD Kit과 수학적 정리 증명 (Verus)

Microsoft Research의 해법은 테스트 케이스를 더 많이 작성하는 것이 아니라, **‘수학적 정리 증명(Mathematical Proof)’**을 도입하는 것입니다.

수학 공식처럼, **“어떤 입력값이 들어오더라도 이 코드는 지정된 명세(Specification)를 100% 만족하며, 허용되지 않은 상태 전이는 절대 일어나지 않는다”**는 명제를 컴파일 타임에 기호적으로 완전히 증명해 버리는 방식입니다.

flowchart TD
    subgraph Workflow ["PDD Kit의 5단계 증명 주도 라이프사이클"]
        direction TB
        P1["1. Plan (기획) : GitHub Next Chopin에서 자연어 의도 협의"]
        P2["2. Spec (명세화) : PDD Kit이 의도를 추출해 Verus 정형 명세로 변환"]
        P3["3. Approve (승인) : 개발자는 코드가 아닌 '명세(Spec)'만을 검토하고 서명"]
        P4["4. Prove (수학적 증명) : Verus + Z3 SMT 솔버가 전 공간 버그 부재 증명"]
        P5["5. Fallback (경험적 검증) : UI/외부 통신 구간은 브라우저 자동화 테스트로 보완"]

        P1 --> P2 --> P3 --> P4 --> P5
    end

2.1 과거에는 왜 어려웠고, 지금은 왜 가능한가?

사실 형식 검증은 새로운 개념이 아닙니다. 하지만 과거에는 우주선 제어 소프트웨어나 암호화 칩 설계 같은 극소수 분야에서만 쓰였습니다. TLA+나 Coq 같은 난해한 증명 언어를 다룰 수 있는 수학자급 전문가가 필요했고, 코드 100줄을 증명하기 위해 수천 줄의 증명 코드를 몇 년 동안 손으로 써야 했기 때문입니다.

2026년 현재, 두 가지 기술적 돌파구가 이 장벽을 무너뜨렸습니다:

에이전트의 증명 코드 작성력: 프론티어 AI 모델이 자연어 명세를 이해하고 고난도의 정형 검증 증명 코드를 스스로 작성할 수 있게 되었습니다.
시스템 언어와 융합된 Verus: Microsoft Research, CMU, ETH Zurich가 공동 개발한 오픈소스 정형 증명 프레임워크인 Verus가 완성되었습니다. Rust의 엄격한 메모리 소유권(Ownership) 모델 위에서 시스템 코드를 직접 검증할 수 있게 된 것입니다.

3. 신뢰 컴퓨팅 기반(TCB)의 실용적 분리

PDD Kit이 뛰어난 점은 현실의 모든 웹 애플리케이션 코드를 100% 수학으로 증명하겠다는 무모한 고집을 부리지 않는다는 데 있습니다.

수학적으로 증명할 수 있는 핵심 영역과, 테스트로 경험적 검증을 해야 하는 영역 사이에 명확한 경계선인 **신뢰 컴퓨팅 기반(TCB, Trusted Computing Base)**을 긋습니다.

flowchart LR
    subgraph Formal ["1. 형식 검증 영역 (Verus 수학적 증명 100%)"]
        F1["인증 및 세션 권한 체크"]
        F2["주문 상태 머신 전이"]
        F3["금융 트랜잭션 잔액 불변성"]
    end

    subgraph TCB ["신뢰 컴퓨팅 경계선 (TCB)"]
        Boundary["인간 개발자가 승인한 정형 명세"]
    end

    subgraph Empirical ["2. 경험적 검증 영역 (테스트 & 브라우저 자동화)"]
        E1["Leptos 프론트엔드 UI 렌더링"]
        E2["SQLite 디스크 I/O 및 데이터베이스"]
        E3["외부 서드파티 암호화 라이브러리"]
    end

    Formal <--> TCB <--> Empirical

형식 검증(Formal Verification): 논리적 허점이 시스템 전체 침해로 이어지는 인증 로직, 세션 만료, 상태 전이, 결제 계산 등은 Verus 수학적 증명에 맡깁니다.
경험적 검증(Empirical Verification): 수학 모델링이 어려운 UI 컴포넌트, 브라우저 DOM 렌더링, 외부 데이터베이스 통신 등은 기존의 단위 테스트 및 브라우저 에이전트 자동화로 처리합니다.
개발자는 TCB 경계선을 확인하고, “이 핵심 로직은 수학적으로 증명되었으니 믿는다”고 안심하고 서명할 수 있습니다.

4. 실전 사례: 풀스택 Rust 웹앱의 로그인 무결성 증명

연구진은 실제 상용 서비스 구조를 갖춘 풀스택 Rust 웹 애플리케이션인 **‘Pet Store’**에 PDD Kit을 적용했습니다.

기술 스택: Axum(백엔드) + SQLite(DB) + Leptos(WebAssembly 프론트엔드), 총 5,000줄의 Rust 코드.
검증 대상: 사용자 로그인 및 세션 핸들러(backend/src/handlers/auth.rs).

개발자가 GitHub Next의 에이전트 기획 도구인 Chopin에 입력한 지시는 아주 간단했습니다:

“auth.rs의 로그인 로직을 검증해 줘. 권한 없는 사용자의 세션 탈취나 잘못된 비밀번호 입력 시 로그인 성공 처리가 절대 발생하지 않아야 해.”

코드를 한 줄도 읽지 않고 버그를 잡다

PDD Kit은 개발자의 의도를 대화식으로 구체화하여 Verus 형식 명세로 변환했습니다. (이때 명세 자체의 빈틈을 잡기 위해 명세 변이 테스트인 Mutation Testing까지 자동으로 수행합니다.)
에이전트가 생성한 구현 코드에 대해 Verus 증명기를 실행하자, 동시성 환경에서 세션이 덮어써질 수 있는 레이스 컨디션 버그와 권한 체크 누락 엣지 케이스가 컴파일 단계에서 즉각 적발되었습니다.
에이전트는 증명 실패 반례(Counter-example)를 전달받아 코드를 수정했고, 마침내 Verus 증명기는 **“명세에 정의된 로그인 버그가 전혀 존재하지 않음(Absence of login bugs)”**을 수학적으로 증명해 냈습니다.
인간 개발자는 에이전트가 작성한 5,000줄의 Rust 코드를 단 한 줄도 눈으로 읽지 않았습니다. 개발자가 검토하고 승인한 것은 오직 **“자신의 원래 의도가 올바른 명세(Spec)로 정확히 변환되었는가”**뿐이었습니다.

5. TDD에서 PDD로: 개발자의 역할은 어떻게 바뀌는가?

지난 20여 년간 현대 소프트웨어 엔지니어링의 표준 상식은 **TDD(Test-Driven Development, 테스트 주도 개발)**였습니다. 실제 구현 코드를 작성하기 전에 실패하는 테스트를 먼저 작성하고(Red), 이를 통과하는 최소한의 코드를 작성한 뒤(Green), 리팩토링(Refactor)하는 3단계 주기를 반복하는 방법론입니다.

flowchart LR
    Red["1. Red (실패)<br/>기능 구현 전 실패하는 단위 테스트 작성"] 
    Green["2. Green (성공)<br/>테스트를 통과하기 위한 최소한의 코드 구현"] 
    Refactor["3. Refactor (개선)<br/>테스트 통과를 유지하며 코드 구조 다듬기"]

    Red --> Green --> Refactor --> Red

TDD의 핵심 믿음은 **“사람이 테스트를 먼저 꼼꼼하게 작성해 두면, 구현 코드가 의도대로 안전하게 만들어졌는지 보장할 수 있다”**는 것이었습니다.

하지만 코딩 에이전트가 수만 줄을 한 번에 찍어내는 시대에는 이 전제가 흔들립니다. 사람이 테스트를 먼저 작성할 시간도 부족할뿐더러, 에이전트에게 테스트를 맡기면 **자신이 잘못 구현한 코드에 꿰맞춘 ‘자기충족적 테스트’**를 작성해 인간의 눈을 속이기 때문입니다.

Microsoft PDD Kit은 샘플 테스트 케이스를 먼저 짜던 TDD에서, 모든 입력 공간에 대한 수학적 정리 증명(Proof)을 먼저 세우는 PDD로의 세대교체를 예고합니다.

구분	전통적 TDD (테스트 주도 개발)	미래형 PDD (증명 주도 개발)
코드 작성 주체	인간 개발자	AI 코딩 에이전트
검증 메커니즘	샘플 입력값 기반의 단위 테스트 실행	가능한 모든 입력값에 대한 수학적 정리 증명 (Verus)
핵심 질문	“내가 넣은 몇 가지 입력값에 대해 코드가 도는가?”	“가능한 모든 상황에서 버그가 없음을 증명할 수 있는가?”
인간의 핵심 역할	코드 타이핑 및 테스트 케이스 작성	자연어 기획 의도 정의 및 정형 명세(Spec) 검토
코드 리뷰 방식	수천 줄의 PR 코드를 한 줄씩 눈으로 읽기	수학적 증명 성공 확인 및 신뢰 경계(TCB) 승인

마치며: 미래의 엔지니어는 코드를 읽지 않습니다

앞으로 코딩 에이전트가 작성하는 코드의 양은 지금보다 10배, 100배 더 늘어날 것입니다. 인간이 그 거대한 코드의 홍수를 두 눈으로 일일이 쫓아가는 방식은 더 이상 지속 가능하지 않습니다.

엔지니어가 집중해야 할 핵심 역량은 에이전트가 짠 for 루프나 함수 구현부를 감상하는 것이 아닙니다. **“비즈니스 기획을 모호함 없는 엄밀한 명세로 정의하고, 기계가 스스로 그 명세를 수학적으로 증명하게 만드는 체계”**를 설계하는 시스템 아키텍트의 시야가 필요한 때입니다.

Microsoft PDD Kit은 에이전트 시대에 인간 개발자가 생산성과 시스템 신뢰성을 동시에 쥐는 가장 명쾌한 길을 보여주고 있습니다.