PDD Kit, Verus로 에이전트 작성 Rust 웹 앱 형식 검증

PDD Kit(Proof-Driven Development Kit)은 자연어 의도를 Verus의 형식 명세로 변환하여 에이전트가 작성한 코드가 모든 입력에 대해 요구사항을 충족하는지 증명함. 이는 AI 생성 코드의 라인별 수동 리뷰가 비현실적이라는 문제를 해결함.
약 5,000줄의 Rust로 작성된 Pet Store 사례 연구에서, 두 문장의 사용자 요청에서 파생된 로그인 로직을 형식적으로 검증함. 이 과정에서 수학적 확실성을 제공하는 형식 증명과 특정 입력에 대한 증거를 제공하는 경험적 테스트를 구분함.
검증 과정은 check_password 및 데이터베이스 조회를 포함한 6개 구성 요소로 구성된 신뢰할 수 있는 계산 기반(Trusted Computing Base, TCB)을 식별함. 이들은 테스트는 되지만 증명되지 않으며, 시스템은 약한 불변 조건을 찾아내기 위해 변이 검사(mutation checking)를 사용함.
현재 Verus를 통해 Rust만 지원하는 연구 프로토타입인 PDD Kit은 GitHub Next의 Chopin 환경과 통합되며 CI에 Verus 검사를 추가함. 이로 인해 증명을 깨뜨리는 코드 변경은 빌드가 실패함.

Verification Mechanics

형식 검증은 Verus(Rust 검증기)를 사용하여 ensures 절과 고스트 코드를 검사하며, 경험적 검증은 증거로 라벨링된 단위 및 끝ToEnd 테스트를 실행함.
login_flow 계약은 8개의 ensures 절을 포함하며, 여기에는 기존 거부 동작(400/401/500)을 유지하는 4개와 올바른 비밀번호로 지정된 계정에만 토큰이 발급되도록 하는 제약 조건이 있음.
모듈형 증명 전략을 통해 login_flow는 더 작은 증명된 조각(lookup_target, login_core, issue_token)으로 구성됨. 하나의 함수를 변경하면 해당 특정 조각만 다시 증명하면 됨.

증명은 모든 입력에 대해 login_flow 및 관련 함수의 본문을 다루지만, 현재 SQLite 상태, 시스템 클럭 시간, 종료 및 성능 보증과 같은 외부 사실은 포함하지 않음.
이 도구는 Verus, Rust 컴파일러, Z3 툴체인이 정확하다고 가정하며, 다른 언어는 Rust로 이식하거나 검증된 Rust를 바인딩을 통해 호출할 수 있음.
도입을 위한 권장 시작점은 로그인, 결제, 권한과 같이 비용이 높은 버그 영역이며, 명확한 명세는 증명 생성에 필요한 노력을 크게 줄여줌.