PDD Kit 검증, AI 코드 검토를 개발자 의도로 전환하다
Microsoft Research는 11월 5일 PDD Kit 검증을 소개하며, 에이전트가 작성한 코드에 형식 검사를 적용하고 인간 검토의 초점을 개발자 의도로 옮기는 방안을 제시했다. 형식 검증은 정의된 가정 아래 코드가 명시적으로 기술된 속성을 충족하는지 수학적 추론으로 확립하는 기법이다. 이 접근이 내세우는 약속은 구체적이다. 에이전트의 구현과 테스트가 원래 요청을 충실히 반영하기를 기대하는 대신, 승인된 요구사항을 강제 가능한 형태로 만드는 것이다.
시연은 Rust로 작성된 풀스택 웹 애플리케이션인 Pet Store의 로그인 로직을 중심으로 한다. Microsoft는 이 워크플로가 Rust용 검증 도구인 Verus를 사용해 생성된 코드를 명세와 대조한다고 밝혔다. 증명 범위 밖의 의존성과 동작은 테스트가 다룬다. 이번 발표가 애플리케이션 전체가 형식 검증됐음을 입증하는 것은 아니다.
참조점은 구현 전에 요구사항을 정리하는 GitHub의 Spec Kit로 대표되는 명세 주도 개발이다. PDD Kit는 이 접근을 기계가 검사하는 의무 조건으로 확장한다. 핵심 질문은 엔지니어링 책임성에 관한 것이다. 에이전트가 구현을 작성할 때, 검토자는 그 구현에 책임을 지기 전에 어떤 증거를 요구해야 하는가?
PDD Kit 검증은 풀스택 앱의 특정 부분을 겨냥한다
Microsoft의 로그인 검증 예시는 임의의 애플리케이션을 위한 범용 보증 서비스가 아니라 연구 프로토타입을 설명한다. 시연된 애플리케이션은 약 5,000줄의 Rust 코드로 구성된다. 보고된 증명은 로그인 로직에 관한 것이며, 다른 구성 요소는 신뢰 대상으로 남아 테스트된다.
핵심 변화는 검토된 요구사항과 기계로 확인된 구현 동작을 연결하는 데 있다.
이 구분은 “풀스택 웹 앱”이라는 표현을 읽을 때 중요하다. 애플리케이션은 검증된 구성 요소를 포함할 수 있지만, 주변의 모든 구성 요소가 같은 보장을 공유하는 것은 아니다. 올바른 로그인 결정이 이후의 모든 관리 작업에서 권한을 올바르게 확인한다는 뜻은 아니다.
Microsoft는 개발자가 생성된 코드를 빠짐없이 읽는 대신 의도를 검토했다고 말한다. 이것이 이 프로젝트의 운영상 제안이다. 인간의 역할은 애플리케이션이 사용자에게 제공해야 할 동작과 팀이 수용할 가정을 결정하는 쪽으로 이동한다.
기능 설명을 승인하는 일과 동작 의무를 승인하는 일의 차이를 생각해 볼 수 있다. “로그인을 안전하게 만들어라”는 목표를 표현하지만, 중요한 결정 대부분은 남겨 둔다. 검토자는 어떤 계정에 접근 권한이 부여되는지, 어떤 조건이 접근을 허용하는지, 실패가 결과를 어떻게 바꾸는지 알아야 한다.
형식 명세, 즉 요구되는 동작을 정확히 기술한 문장은 선택된 결정을 기계적으로 검사할 수 있을 만큼 명확하게 만든다. 또한 누락도 드러낸다. 특정 동작을 전혀 다루지 않는 요구사항은 검증기가 그 동작을 거부할 근거를 제공하지 않는다.
이 구분은 독자가 시연을 평가하는 방식도 바꾼다. 그 중요성은 요구사항과 코드 사이에 검증 가능한 관계가 있다는 데 있다. 상점을 완전히 안전하다고 제시하거나 인간 검토가 더는 필요 없다고 선언하는 데 있지 않다.
따라서 가장 강한 해석은 점진적이다. 팀은 엄격하게 정의된 중요한 애플리케이션 로직이 증명 의무의 이점을 얻는지 조사할 수 있다. 그다음 그러한 의무 밖에 남는 주변 동작이 얼마나 많은지 살펴볼 수 있다.
이 접근은 발표의 주장을 과도하게 확장하지 않으면서 실용적인 틀을 제공한다. 로그인 구성 요소는 의도 검토가 작동하는지 조사할 구체적인 지점을 제공한다. 애플리케이션 신뢰성에 관한 더 광범위한 주장은 더 폭넓은 증거를 필요로 한다.
또한 분석에 적절한 경계를 설정한다. 이 워크플로가 명세된 동작에 대한 보증을 높이는 동시에 남은 불확실성을 계속 드러내는지가 질문의 핵심이다.
엔지니어링 책임자는 명세 문제를 떠안는다
즉각적인 부담은 생성된 변경 사항을 승인하는 사람들에게 돌아간다. 검토자는 여전히 소프트웨어가 조직이 요청한 일을 수행한다고 믿을 만한 근거가 필요하다. 더 많은 구현 세부 사항을 생성한다고 해서 그 근거가 자동으로 생기는 것은 아니다.
의도를 검토한다는 것은 요구사항 품질을 운영상의 책임으로 만든다.
기존 검토에서는 구현을 면밀히 살펴보는 과정에서 명시되지 않은 규칙을 발견할 수 있다. 검토자는 특이한 계정 상태에 특별한 처리가 필요하다는 점을 알아챌 수 있다. 구현에서 시선을 옮길수록 그러한 규칙을 의도적으로 발견하는 일이 더 중요해진다.
이는 측정된 도입 결과가 아니라 제안된 워크플로의 함의다. 요구사항이 기계가 코드를 판단하는 기준이 된다면, 불완전한 요구사항은 잔여 위험의 핵심 원인이 된다.
따라서 제품 책임자와 보안 검토자는 소프트웨어 보증에서 더 직접적인 역할을 맡게 된다. 이들은 코드가 때로 숨기는 비즈니스 결정을 해결해야 한다. 엔지니어는 그러한 결정을 정확히 표현됐을 때도 의미를 유지하는 문장으로 옮겨야 한다.
예를 들어 계정 복구 기능은 그 어려움을 보여 준다. 비즈니스 요청은 검증된 사용자가 접근 권한을 되찾아야 한다고 말할 수 있다. 그러나 명세는 여전히 검증의 정의, 만료된 요청, 충돌하는 계정 상태, 이전 승인을 무효화하는 상황을 정해야 한다.
해결되지 않은 각 용어는 구현이 그럴듯한 해석을 따르면서도 요청자를 실망시킬 여지를 만든다. 형식 검사는 선택된 해석을 강제할 수 있다. 그 해석을 선택하는 일은 여전히 인간의 결정이다.
Shuvendu Lahiri의 의도 형식화 연구는 명세 검증을 핵심 과제로 지목한다. 이 연구는 명세의 정확성에는 자동 오라클이 없기 때문에 비형식적 의도를 검사 가능한 요구사항으로 옮기는 과정에 사용자 참여가 필요하다고 주장한다.
이 연구는 발표를 바라보는 데 유용한 회의적 관점을 제공한다. 성공적인 증명은 팀이 올바른 목표를 선택했는지를 판정할 수 없다. 그것은 구현과 서면 의무 사이의 관계를 확립한다.
엔지니어링 관리 측면에서는 검토 노력을 평가하는 다른 방식이 제시된다. 요구사항을 명확히 하는 데 쓰는 시간은 전달 프로세스의 일부로 간주해야 한다. 이후 코드 읽기 노력이 줄어든다면, 그 효과는 앞선 투자와 함께 평가해야 한다.
출시 후의 책임에도 같은 원칙이 적용된다. 요구사항이 바뀌면 누군가는 형식 의무도 함께 바꿔야 하는지 결정해야 한다. 명세를 지속적인 기술 산출물로 취급하려면 책임 있는 소유자가 필요하다.
여기서 결정 이력이 유용해진다. 팀은 승인된 예외, 의존성 가정 또는 실패 정책의 배경 이유에 접근할 수 있어야 한다. 검색 가능한 지식 베이스는 기술 문서 전반에서 이러한 연속성을 지원할 수 있다.
문서만으로 정확성 보장을 제공할 수는 없다. 문서의 기여는 향후 검토자가 기존 보장이 여전히 의도된 동작을 표현하는지 판단할 수 있도록 맥락을 보존하는 데 있다.
더 넓은 결과는 조직적이다. 기업이 기계가 자사의 요구사항을 강제하기를 원한다면, 먼저 그 요구사항을 책임질 수 있을 만큼 명확하게 만들어야 한다.
규칙과 그 의미 사이의 간극으로 설명하는 PDD Kit
GitHub Next의 증명 주도 개발 설명은 PDD Kit를 협업형 계획 환경인 Chopin 안의 계획 파트너로 소개한다. 이 도구는 인간의 요구사항을 명세와 테스트에 연결하는 의도 아티팩트에 결정을 기록한다.
이 설명은 드러나는 모호성도 보여 준다. 올바른 비밀번호를 가진 경우에만 토큰을 허용하는 규칙은 모든 로그인을 거부하는 시스템도 허용한다. 무단 접근 방지와 정당한 접근 허용에는 서로 다른 의무가 필요하다.
명세는 허용할 수 없는 동작을 배제하면서도 사용자가 필요로 하는 서비스를 실수로 배제하지 않아야 한다.
이 예시는 정확성에 관한 추상적 주장보다 작동 방식을 더 분명히 설명한다. 어떤 규칙은 대화에서는 완전해 보이지만, 논리적으로는 유효해도 아무도 원하지 않는 구현을 남길 수 있다.
같은 추론은 로그인 밖에도 적용된다. 승인되지 않은 계정에 절대 청구해서는 안 되는 가상의 결제 서비스를 생각해 보자. 결제를 전혀 처리하지 않는 서비스는 그 제한을 충족한다. 상업적으로 유용한 서비스에는 유효한 결제를 규정하는 요구사항도 필요하다.
이 예시들은 추가 PDD Kit 시연이 아니라 추론 연습이다. 요구사항에는 방지하려는 실패뿐 아니라 성공적인 동작이 무엇인지에 관한 긍정적 의무도 필요함을 보여 준다. 팀은 성공적인 동작의 의미를 설명해야 한다.
이러한 결정이 형식 의무가 되면 검증기는 구현을 그에 맞춰 검사한다. Rust 검증 프로젝트에 따르면 Verus는 런타임 검사를 삽입하는 대신 실행 전에 정적으로 명세를 검사한다. 현재 Rust의 일부만 지원하며, 여전히 활발히 개발되고 있다.
이 아키텍처는 답안을 생성하는 일과 그것을 수용하는 일을 분리한다. 에이전트는 구현과 이를 뒷받침하는 증명을 제안할 수 있다. 기계적 검증은 지원되는 모델 안에서 명시된 의무가 성립하는지를 판단한다.
유창한 설명은 구현 정확성의 약한 증거이므로 이 구분은 중요하다. 에이전트는 한 분기를 간과하면서도 의도한 동작을 설득력 있게 설명할 수 있다. 기계적 의무는 그 분기가 충족해야 할 정의된 조건을 부여한다.
그러나 정확성만으로 유용한 범위가 보장되지는 않는다. 가령 가상의 계약이 반환된 계정 식별자는 기대되는 데이터 유형이어야 한다고 말한다고 하자. 그 요구사항은 식별자가 잘못된 계정에 속하더라도 충족될 수 있다.
더 강한 계약은 결과를 요청으로 확립된 신원 및 수용된 인증 조건과 연결할 것이다. 중요한 속성은 개별 값의 외형이 아니라 값들 사이의 관계에 관한 것이다.
이 때문에 PDD Kit 검증은 요구사항 수준에서 평가할 가치가 있다. 녹색 결과는 검토자가 검사된 문장이 무엇을 금지하고 요구하는지 이해할 때만 의미를 갖는다.
실용적 경계도 중요하다. 지원되지 않는 구성 요소와 의존성은 주변 코드의 직접 검증을 막을 수 있다. 그러면 팀은 어떤 보장이 해당 구성 요소에 관한 가정에 의존하는지 분명히 설명해야 한다.
이는 계층적 논거를 남긴다. 인간의 판단은 의도된 동작을 선택한다. 형식 문장은 선택된 의무를 표현한다. 기계적 검사는 수용된 가정 아래 구현과 그 의무의 관계를 확립한다.
어느 계층이든 독자가 기대하는 보증을 제공하지 못할 수 있다. 가치는 검토자가 그 관계를 살필 수 있도록 이러한 계층을 충분히 명확하게 드러내는 데 있다.
이처럼 설명되는 PDD Kit은 명시적인 행동 약속을 중심으로 책임성을 정리하려는 시도다. 그 성공은 애플리케이션이 변화하는 과정에서도 이러한 정리가 이해하기 쉬운 상태로 유지되는지에 달려 있다.
PDD Kit과 테스트의 비교는 증거의 문제다
테스트와 형식 검증은 서로 다른 종류의 증거를 확립한다. 테스트는 선택된 상황을 실행하고 관찰된 결과를 확인한다. 증명은 자신의 모델과 가정이 포괄하는 입력 및 실행 전반에 걸쳐 명시된 속성을 확립한다.
유용한 비교는 각 검사가 어떤 주장을 뒷받침하는지 묻는 것이다.
브라우저 테스트는 특정 로그인 흐름이 테스트 환경에서 작동했음을 보여줄 수 있다. 손상된 양식, 예상치 못한 응답, 또는 구성 요소 연결 실패를 드러낼 수 있다. 선택된 내부 로직에 증명이 있더라도 이러한 관찰은 여전히 가치가 있다.
형식적 의무는 다른 질문을 다룰 수 있다. 모델링된 의사결정 로직이 금지된 결과를 허용하는 경우가 있는지다. 이러한 보장은 명세와 검사 대상 코드 주변의 경계에 달려 있다.
어느 결과도 다른 결과의 범위를 암묵적으로 물려받아서는 안 된다. 성공한 브라우저 흐름이 가능한 모든 로그인 결과를 입증하지는 않는다. 의사결정 함수에 관한 증명이 배포된 페이지가 의도한 요청을 전송한다는 사실을 입증하지도 않는다.
GitHub의 specification-driven development 툴킷은 가까운 비교 기준을 제공한다. Spec Kit은 코딩 에이전트를 위한 명세, 계획, 구현, 검토 프로세스를 구성한다. 문서는 구조화된 워크플로와 검증 결과를 설명하지만, 모든 명세를 수학적 증명으로 만들지는 않는다.
여기서의 차이는 프로세스 지침과 특정 형태의 증거 사이에 있다. 구조화된 계획은 협업을 개선하고 누락된 작업을 드러낼 수 있다. 형식적 의무는 표현된 행동에 대해 기계적으로 확인 가능한 관계를 추가한다.
이 차이를 명세 주도 팀에는 강제가 없다는 포괄적 주장으로 확대하는 것은 오해를 부를 수 있다. 팀은 계획에 테스트, 분석, 검토 게이트 및 기타 검사를 연결할 수 있다. 문제는 그러한 검사가 실제로 무엇을 확립하는가에 있다.
Amazon의 verification-guided development 작업도 또 다른 비교 사례를 제공한다. Cedar 연구는 실행 가능한 모델에 관한 증명과 구현을 비교하는 차등 테스트, 그리고 생성된 사례를 검사하는 속성 기반 테스트를 결합한다.
Cedar 논문은 증명을 통해 정책 검증기 버그 4건을, 테스트를 통해 추가로 21건의 버그를 발견했다고 보고한다. 이 발견은 PDD Kit이 아닌 Cedar에 관한 것이며, 제품 간 성능 비교를 입증하지는 않는다.
다만 더 넓은 공학적 입장을 뒷받침하는 증거는 제공한다. 증명과 테스트는 상호 보완적인 발견에 기여할 수 있다. 서로 다른 기법은 동일한 개발 노력 안에서 서로 다른 결함을 드러낼 수 있다.
에이전트 보조 개발을 평가하는 구매자에게 실질적인 질문은 더 구체적이다. 요구사항은 이를 구현하는 코드와 어떤 증거로 연결되는가? 그 연결은 어디에서 테스트, 가정 또는 사람의 검토에 의존하는가?
이는 제품이 일반적으로 검증을 지원하는지 묻는 것보다 더 유용한 도입 검토 논의다. 이 용어는 강도와 범위가 서로 다른 주장을 포괄한다.
그러므로 PDD Kit과 테스트의 비교는 보증 지도로 마무리되어야 한다. 검토자는 어떤 요구사항에 증명이 있는지, 어떤 요구사항에 실행된 검사가 있는지, 그리고 어떤 부분이 여전히 판단의 영역인지 확인할 수 있어야 한다.
검증된 구성 요소도 주변 환경에 의존한다
PDD Kit 검증이 경계를 살펴볼 필요를 없애지는 않는다. 신뢰 컴퓨팅 기반은 보장이 의존하는 구성 요소와 가정의 집합이다. 수용된 가정이 실패하면 증명은 여전히 유효할 수 있지만, 기대한 애플리케이션 동작은 실패할 수 있다.
보장 범위는 증명이 통과했다는 사실만큼 중요하다.
Microsoft의 설명에서는 데이터베이스 조회, 비밀번호 검사, 시계 접근, 토큰 서명, 요청 처리가 제시된 증명 밖에 놓여 있다. 이러한 구성 요소에는 테스트와 수용된 계약이 적용된다. 증명은 그 구현의 정확성을 독립적으로 확립하지 않는다.
이 제한은 주변 구성 요소가 추상적 결정을 실제 신원 및 실제 요청과 연결하기 때문에 중요하다. 올바른 내부 결정에는 정확한 정보가 필요하다. 또한 의도된 실행 경로를 통해 결과가 전달되어야 한다.
성공을 보고하면서도 잘못된 계정을 반환하는 가상의 조회를 생각해 보자. 하위 함수는 그 결과를 명세대로 정확히 처리할 수 있다. 그럼에도 수용된 의존성 가정이 실패했기 때문에 전체 동작은 사용자 기대를 충족하지 못한다.
이는 보고된 Pet Store 결함이 아니라 일반적인 추론 사례다. 가정을 부차적인 문서로 취급하지 말고 살펴봐야 하는 이유를 보여준다.
같은 구분은 누락된 요구사항에도 적용된다. 접근 결정에 초점을 둔 명세가 응답성, 악용 방지 제어 또는 계정 복구를 자동으로 다루지는 않는다. 각각의 추가 주장은 고유한 뒷받침 논거가 필요하다.
이 점은 중요한 보도 원칙을 만든다. “검증된 로그인 로직”은 실제 속성과 경계에 계속 연결되어야 한다. 이 표현을 “안전한 인증 시스템”으로 확장하면, 제시된 증거가 반드시 뒷받침하지 않는 주장이 추가된다.
도입의 문제도 있다. Rust 전용 검증은 이 프로토타입이 직접 적용될 수 있는 범위를 제한한다. 다른 애플리케이션 언어를 사용하는 조직은 같은 워크플로가 적용될 것이라 기대하기 전에 통합 작업을 고려해야 한다.
그러한 작업이 존재한다고 해서 접근 방식이 실용적이지 않은 것은 아니다. 비용과 편익의 계산이 구성 요소, 그 결과의 중요성, 그리고 행동을 표현하는 데 필요한 노력에 달려 있음을 의미한다.
실패 비용이 큰 소규모 구성 요소는 상당한 명세 작업을 정당화할 수 있다. 자주 변경되는 인터페이스에는 다른 균형이 필요할 수 있다. 이는 PDD Kit의 경제성에 관한 측정된 결론이 아니라 평가 고려사항이다.
독자는 워크플로 시연과 독립적 검증도 구분해야 한다. Microsoft와 GitHub Next의 설명은 저자들의 시스템과 경험을 소개한다. 관련 없는 여러 프로덕션 팀 전반의 결함 감소를 일반적으로 확립하지는 않는다.
프로토타입이라는 표기는 추가 조사의 여지를 남긴다. 반복 사용, 유지보수 노력, 검토자의 이해도에 관한 질문을 제기한다. 이러한 질문에 답하려면 초기 애플리케이션 사례를 넘어서는 증거가 필요하다.
합리적인 기준은 엄격하지만 구체적이다. 검토자는 약속된 행동, 수용된 의존성, 제외된 주장, 그리고 각 항목에 연결된 증거를 이해할 수 있어야 한다.
이 기준은 누구에게나 좁은 증명을 완전한 애플리케이션 보증과 동일시하도록 요구하지 않으면서도 신중한 실험을 뒷받침한다.
다음 증거는 재현, 경계, 유지보수를 다뤄야 한다
다음 전개는 이 워크플로가 초기 시연을 넘어 확장되는지 분명히 해야 한다. 앞으로 몇 달 동안 세 가지 신호를 정해진 순서로 주목할 필요가 있다. 독립적 재현, 의존성 범위, 그리고 유지보수 동작이다.
가장 강력한 도입 증거는 소프트웨어가 변화하는 동안에도 팀이 의미 있는 보장을 유지할 수 있음을 보여줄 것이다.
첫째, 서로 다른 요구사항을 가진 애플리케이션 로직에서 독립적인 팀이 워크플로를 재현하는지 살펴봐야 한다. 유용한 설명은 시작 요청, 수용된 명세, 그에 따른 검사, 모호성을 해결하는 데 필요한 노력을 식별해야 한다.
성공적인 재현은 계획 방식이 제작자를 넘어 이전될 수 있다는 근거를 강화한다. 공개되지 않은 전문가 개입에 반복적으로 의존한다면 그러한 해석은 좁아진다.
중요한 신호는 다른 환경에서 나온 이해 가능한 증거다. 완성도 높은 시연만으로는 익숙하지 않은 팀이 상충하는 요구사항이나 오해한 가정을 어떻게 다루는지 알 수 없다.
둘째, 프로젝트가 신뢰하는 의존성을 어떻게 설명하고 관리하는지 살펴봐야 한다. 진전은 추가 행동을 증명에 포함하는 것을 의미할 수 있다. 여전히 증명 밖에 남는 구성 요소를 위해 더 명확하고 재현 가능한 검사를 만드는 것도 진전을 의미할 수 있다.
새 증명이 의미 있는 속성을 다룬다면 더 작은 경계는 선택된 보장을 강화할 수 있다. 더 명확한 경계는 검토자가 남은 위험을 판단하는 능력을 높인다.
어느 발전도 구성 요소 수만으로 평가해서는 안 된다. 의존성의 결과는 서로 다르다. 영향이 작은 보조 기능을 검증된 코드로 옮긴다고 해서 가장 중요한 불확실성이 반드시 줄어드는 것은 아니다.
더 드러나는 질문은 어떤 애플리케이션 약속이 여전히 증명되지 않은 행동에 의존하는가이다. 그 관계를 보고하면 향후 시연을 더 쉽게 평가할 수 있다.
셋째, 일상적인 요구사항 변경 중 어떤 일이 일어나는지 살펴봐야 한다. 성숙한 평가는 새 행동에 수반되는 명세 결정을 포함해 초기 수용 이후의 구성 요소를 추적해야 한다.
가상의 팀이 계정 정책을 변경한다고 가정해 보자. 흥미로운 결과는 검토자가 의도된 정책 개정과 구현 회귀를 구분할 수 있는지다. 실패한 검사는 어떤 산출물을 바꿔야 하는지에 관한 정보에 기반한 결정으로 이어져야 한다.
안정적이고 이해하기 쉬운 유지보수의 증거는 운영 측면의 근거를 강화한다. 빌드가 결국 성공하더라도 통과 검사를 복구하기 위해 요구사항을 반복적으로 약화한다면 그 근거는 약화된다.
잠재적 사용자에게 이 신호들은 평가 방법을 제시한다. 범위가 제한된 구성 요소를 선택하고, 중요한 행동을 식별한 뒤, 그 구현을 수용하는 데 어떤 증거가 필요한지 물어야 한다.
요구사항 검토, 가정 이해, 검사 유지보수의 비용도 포함해야 한다. 이러한 활동은 코드 읽기 노력 감소와 같은 평가에서 함께 다뤄져야 한다.
주장은 증거에 비례하게 유지해야 한다. 워크플로는 주변 제품 전체에 대한 완전한 보증을 제공하지 않으면서도 중요한 구성 요소에 대한 신뢰를 높일 수 있다.
PDD Kit 검증을 도입하기 전에, 팀이 이미 명확하다고 여기는 요구사항 하나를 살펴보자. 제품 책임자와 엔지니어에게 성공적인 결과와 수용할 수 없는 결과를 각각 설명하게 하라. 증명을 논의하기 전에 답변을 비교하라. 그다음 어느 설명이든 성립하려면 올바르게 동작해야 하는 의존성을 식별하라. 이 연습은 구현을 검증하지는 않지만, 검증 워크플로가 보존해야 할 결정을 드러낼 것이다. 이러한 결정을 염두에 두고 기술 설명을 읽고, 각 약속과 그 증거 사이의 명시적 연결을 찾아야 한다. 다음 평가를 위한 유용한 질문은 구체적이다. 검토자는 소프트웨어가 무엇을 보장하는지, 왜 그것을 믿는지, 그리고 무엇이 그 보장 밖에 남아 있는지 설명할 수 있는가?
