검증할 속성
0 ≤ refunded + amount ≤ paid
- 대상: 환불 정책 함수 하나
- 입력: 음수가 아닌 정수
- 외부 I/O, DB, 네트워크는 범위 밖
- 명시한 가정과 Go 하위 집합 안에서 확인
MPK Assurance / Go 증명 준비도 리뷰
Go 코드를 테스트에 그치지 않고
증명합니다.
환불, 수수료, 잔액, 준비금처럼 돈을 움직이는 중요한 Go 로직을 명시한 사양, 가정, 범위와 대조해 기계적으로 확인합니다. Gemini가 증명 후보를 준비하고, 독립적인 MPK 커널이 최종 판정을 내립니다.
선착순 5개사 한정 MPK 조기 도입 제안 JPY 49,800(세전)Go 함수 하나에서 시작
최대 2개 속성
기밀 코드를
공개 입력하지 않음
공개 입력하지 않음
재검증 가능한
증거 제공
증거 제공
refund.go
func ApplyRefund(paid, refunded, amount int64) (int64, error) {
if amount < 0 {
return refunded, errors.New("negative amount")
}
if refunded+amount > paid {
return refunded, errors.New("exceeds paid")
}
return refunded + amount, nil
}검증할 속성
∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid
반례 발견
paid=100, refunded=80, amount=30이 속성을 위반합니다.
커널 검증 완료
커널이 수정된 표준 인증서를 승인했습니다.
테스트를 넘어선 보증일반 Go 코드에서 시작AI와 신뢰 판단을 분리증명, 반례, 제외 범위 제시
30초 환불 데모
반례를 찾은 뒤 수정된 버전을 증명합니다.
준비된 환불 코드를 사용해 반례, 수정, 증명 성공까지의 흐름을 확인하십시오. 공개 데모에 기밀 코드를 입력할 필요는 없습니다.
환불 정책: 누적 환불액은 결제 금액을 초과할 수 없습니다
검증 결과 (버그가 있는 구현)
반례 발견
누적 환불액이 결제 금액을 초과하는 구체적인 입력을 찾았습니다.
paid = 100
refunded = 80
amount = 30
result = 110 (속성 위반)
refunded = 80
amount = 30
result = 110 (속성 위반)
기술 세부 정보
- 실행 ID
- run_refund_bug_20260727
- 인증서 해시
- — 반례가 발견되어 생성되지 않음
- 커널 판정
- 거부 / 반례
- 공리 보고서
- 정수 산술 / 명시한 가정
결과 분류
네 가지 결과 유형
증명됨
지정한 속성이 명시한 가정과 범위 안에서 성립합니다.
증명됨반례 발견
속성을 위반하는 구체적인 입력을 보여주고 어떤 조건을 수정해야 하는지 명확히 합니다.
반례판정 불가
현재 전략으로 속성 성립 여부를 판단할 수 없을 때 이를 명확히 보고합니다.
판정 불가범위 밖
지원하지 않는 문법, 외부 I/O, 미지원 동작처럼 대상을 다룰 수 없는 구체적인 이유를 설명합니다.
적용 불가테스트와의 차이
선택한 입력만이 아니라 지정한 속성을 확인합니다.
테스트(예시 기반)
- 작성한 케이스만 실행
- 선택하지 않은 입력은 확인되지 않음
- 통과 결과가 인증서는 아님
- 신뢰가 테스트 설계에 의존
MPK Assurance(증명)
- 지정한 속성과 범위를 확인
- 속성을 깨는 구체적인 입력을 제시
- 재검증 가능한 인증서와 해시를 남김
- 독립적인 커널이 최종 판정
| 비교 | 테스트 | 증명 |
|---|---|---|
| 대상 | 선택한 입력 | 지정한 속성 |
| 반례 표시 | △ | ○ |
| 재검증 | 실행 로그 | 인증서 |
| 최종 판단 | 테스트 스위트 | 커널 |
세 가지 특징
테스트를 넘어선 보증
몇 개의 샘플 입력만이 아니라 명시한 사양, 가정, 범위에 대해 속성을 확인합니다.
특수 증명 언어가 아니라 Go를 사용
외부 I/O에서 분리한 중요한 Go 정책 함수부터 시작할 수 있습니다.
AI가 증명하게 하되 AI를 신뢰하지 않습니다
AI는 후보만 준비합니다. 최종 승인은 표준 인증서를 읽는 독립적인 커널이 수행합니다.
작업은 AI에 맡기되, 최종 판단은 AI에 맡기지 마십시오.
고객Go 함수와 보증할 속성을 제출
Gemini속성, 전략, 증명 후보 제안
MPK인증서를 독립적으로 확인하는 신뢰 경계
사람사양, 가정, 기밀 취급 확인
증거재검증 가능한 증거 패키지 제공
Gemini가 증명 워크플로를 실행하고, MPK가 신뢰 판단을 내리며, 사람이 납품을 승인합니다.
검증이 도움이 되는 사용 사례
환불누적 환불액은 결제 금액을 초과할 수 없음
수수료음수가 되지 않고 계약 한도를 넘지 않음
준비금처리 후 잔액이 최소 기준 아래로 내려가지 않음
할인할인이 중첩되어도 한도 안에 유지
포인트발행 포인트가 예산 한도를 초과하지 않음
분배분배 금액 합계가 원래 원금과 일치
증거 패키지
AI의 답변이 아니라 재검증 가능한 증거를 제공합니다.
FINITE FIELD
MPK 인증서
증명 준비도 리뷰
표준 인증서 기록
커널 판정
승인됨
승인됨
MPK
- 인증서 해시
- MPK 커널 판정
- Go 참조 체커 결과
- 공리 보고서
- 증명된 속성과 명시한 가정
- 제외 범위와 범위 밖 사유
- 발견된 반례
- 실행 ID와 재검증 정보
증명 준비도 리뷰
고정된 범위 안에서 첫 번째 함수를 검토합니다.
JPY 198,000 (세전)
- Go 함수 하나
- 증명할 속성 최대 2개
- 결과를 증명됨, 반례, 판정 불가, 범위 밖으로 분류
- 증거 패키지와 결과 온라인 설명
이는 예정된 일반가입니다. 현재 선착순 5개사 한정으로 세전 JPY 49,800의 조기 도입 캠페인을 진행하고 있습니다.
MPK 조기 도입 제안
선착순 5개사 한정중요한 Go 코드가 테스트를 넘어 증명 가능한지 확인하십시오.
MPK 증명 준비도 리뷰에서는 대상 Go 함수 하나를 선택하고, 보증할 속성을 정의하며, AI로 증명 후보를 생성한 뒤 MPK 커널로 독립 검사를 실행합니다.
포함 내용
- Go 함수 하나
- 증명할 속성 최대 2개
- MPK 적합성 평가
- 증명, 반례, 증명 저해 요인, 범위 밖 항목에 대한 보고서
- 증명 범위와 가정을 요약한 보고서
캠페인 조건
이 제안은 서비스 후 솔직한 피드백을 제공하고 MPK 공식 사이트에 게시할 사례 공개를 승인할 수 있는 회사를 대상으로 합니다. 사례에는 회사명, 담당자명, 직함, 피드백, 대표 사진 또는 회사 로고가 포함될 수 있습니다.
회사명이름직함피드백대표 사진 또는 회사 로고
게시 전 내용을 확인해 주시며, 승인된 자료만 사용합니다. 호의적인 평가를 요구하지 않습니다.
서비스 흐름
서비스 흐름(5단계)
발견
손실을 일으킬 수 있는 실패 시나리오와 대상 함수를 확인합니다.
범위 확정
함수, 속성, 가정, 제외 범위를 확정합니다.
Gemini + MPK 리뷰
AI가 후보를 준비하고 MPK가 인증서를 확인합니다.
결과 설명
증명, 반례, 판정 불가 결과, 제외 항목, 증거를 함께 확인합니다.
다음 단계
수정, 추가 함수, CI/CD 통합 중 어디로 진행할지 명확히 합니다.
적합한 경우
- Go로 환불, 수수료, 잔액 로직을 구현하고 있음
- 결함 하나가 금전 손실이나 감사 부담으로 이어질 수 있음
- 전담 형식 검증 팀이 없음
- 외부 I/O에서 분리할 수 있는 작은 함수가 있음
현재 한계
- 임의의 Go 애플리케이션 전체 증명
- DB, API, 네트워크, UI를 포함하는 엔드투엔드 처리
- 모든 보안 취약점 탐지
- 지원하지 않는 문법, 외부 의존성, 불명확한 사양
FAQ
첫 상담 전 FAQ
증명 범위, AI의 역할, 코드 취급 방식 등 문의 전에 자주 나오는 질문을 정리했습니다.
모든 버그가 없어집니까?
아니요. 명시한 가정, 범위, 지원되는 Go 하위 집합 안에서 지정한 속성만 확인합니다. 애플리케이션 전체나 외부 시스템을 보증하지 않습니다.
Lean이나 Rocq를 배워야 합니까?
첫 리뷰에서는 필요하지 않습니다. 외부 I/O에서 분리된 Go 정책 함수와 보증하려는 속성을 확인하는 것부터 시작합니다.
AI가 무엇이 올바른지 결정합니까?
아니요. Gemini는 속성, 증명 전략, 증명 후보를 만듭니다. 독립적인 MPK 커널이 최종 인증서를 승인하거나 거부합니다.
증명에 실패하면 어떻게 됩니까?
결과를 반례, 판정 불가, 범위 밖으로 분류한 뒤 이유, 필요한 사양, 가능한 수정 방향, 증명 가능한 단위를 분리하는 방법을 설명합니다.
CI/CD에 통합할 수 있습니까?
증명 준비도 리뷰에서 대상과 증명 가능성이 확인되면, 지속 검증 또는 CI/CD 통합을 별도로 제안할 수 있습니다.
문의할 때 코드를 보내야 합니까?
공개 양식에 기밀 코드를 붙여 넣을 필요는 없습니다. 문의 후 NDA 처리와 안전한 공유 방법을 확인합니다.
문의
코드가 증명 가능한지 확인하십시오.
가장 중요한 실패가 무엇인지, 어떤 Go 함수를 검토하고 싶은지 알려주십시오. 공개 양식에 기밀 코드를 붙여 넣을 필요는 없습니다.
NDA와 안전한 코드 공유 지원