待驗證性質
0 ≤ refunded + amount ≤ paid
- 目標：1 個退款策略函式
- 輸入：非負整數
- 外部 I/O、DB、網路不在檢查範圍內
- 在明確列出的假設和 Go 子集內檢查
MPK Assurance / Go 證明可行性審查
我們不只是測試，
而是證明你的 Go 程式碼。
針對退款、手續費、餘額、準備金等涉及資金流轉的關鍵 Go 邏輯，我們會依照明確的規格、假設和檢查範圍進行機械式檢查。Gemini 產生證明候選，MPK 獨立核心做出最終判定。
限前 5 家公司 MPK 早期導入方案 49,800 日圓（未稅）從 1 個 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
- 憑證雜湊
- —（因發現反例而未產生）
- 核心判定
- 已拒絕 / 發現反例
- 公理報告
- 整數算術 / 明確假設
結果分類
結果分為 4 類
已證明
指定性質在明確的假設和檢查範圍內成立。
已證明發現反例
展示破壞性質的具體輸入，並明確需要修正的條件。
已發現反例無法判定
明確報告目前策略無法判定性質是否成立。
無法判定超出範圍
具體說明無法處理的原因，例如暫不支援的語法、外部 I/O 或功能限制。
超出範圍與測試的區別
檢查指定性質，而不只是少量選定輸入。
測試（範例式）
- 執行寫好的用例
- 未覆蓋的輸入仍然存在
- 測試通過並不等於證明憑證
- 信任依賴測試設計
MPK Assurance（證明）
- 檢查指定性質及範圍
- 具體展示破壞性質的輸入
- 留下可重新檢查的憑證和雜湊
- 獨立核心做最終判定
| 比較 | 測試 | 證明 |
|---|---|---|
| 對象 | 選定輸入 | 指定性質 |
| 反例顯示 | △ | ○ |
| 重新檢查 | 執行日誌 | 憑證 |
| 最終判斷 | 測試套件 | 核心 |
3 個特點
超越測試的保證
不是只執行少量範例輸入，而是在明確的規格、假設和檢查範圍內檢查性質。
使用 Go，而不是特殊證明語言
可以從與外部 I/O 分離的關鍵 Go 策略函式開始。
讓 AI 證明，但不信任 AI
AI 只負責產生候選。最終是否接受，由讀取標準化憑證的獨立核心決定。
讓 AI 工作，但不讓 AI 做最終判斷。
客戶提交 Go 函式和想保證的性質
Gemini提出性質、策略與證明候選
MPK獨立檢查憑證的信任邊界
人確認規格、假設與機密性
證據交付可重新檢查的證據包
Gemini 執行證明流程；MPK 做信任判定，經人工確認後交付。
適合驗證的用例
退款累計退款額不得超過支付金額
手續費不為負，且不超過合約上限
準備金處理後餘額不低於最低額
折扣多個折扣疊加也不超過上限
積分發放量不超過預算上限
分帳分帳總額與原始金額一致
證據包
交付的是可重新檢查的證據，而不是 AI 的回答。
Finite Field
MPK 憑證
證明可行性審查
標準化憑證記錄
核心判定
已接受
已接受
MPK
- 憑證雜湊
- MPK 核心判定
- Go 參考檢查器結果
- 公理報告
- 已證明的性質與明確列出的假設
- 排除範圍與超出範圍原因
- 反例（如發現）
- 執行 ID 與重新檢查資訊
證明可行性審查
在固定範圍內審查第一個函式。
198,000 日圓 （未稅）
- 1 個 Go 函式
- 最多 2 項待證明性質
- 將結果歸類為已證明、發現反例、無法判定或超出範圍
- 證據包與線上結果說明
這是預定標準價格。目前正在提供限前 5 家公司、49,800 日圓（未稅）的早期導入方案。
MPK 早期導入方案
限前 5 家公司確認貴公司的關鍵 Go 程式碼 是否能 不只通過測試，還能被證明。
在 MPK 證明可行性審查中，我們選擇一個目標 Go 函式，整理要保證的性質，由 AI 產生證明候選，再由 MPK 核心獨立檢查。
服務內容
- 1 個 Go 函式
- 最多 2 項待證明性質
- MPK 適用性診斷
- 說明證明結果、反例、證明障礙或超出範圍原因
- 彙總證明範圍與假設的報告
方案適用條件
本方案提供給願意在服務完成後提供坦率回饋，並核准在 MPK 官方網站發布案例的公司。案例內容可包括公司名稱、姓名、職稱、回饋，以及負責人照片或公司標誌。
公司名稱姓名職稱回饋負責人照片或公司標誌
所有發布內容都會在公開前請您確認，只使用已獲核准的內容。我們不會要求正面評價。
服務流程
服務流程（5 步）
需求確認
確認可能造成損失的失敗情境和目標函式。
確定範圍
鎖定函式、性質、假設和排除範圍。
Gemini + MPK 審查
AI 產生候選，MPK 檢查憑證。
結果說明
講解證明、反例、無法判定、排除項目和證據。
下一步建議
明確後續是否進入修正、更多函式或 CI/CD 整合。
適合以下公司
- 使用 Go 實現退款、手續費或餘額邏輯
- 一個錯誤就可能帶來資金損失或稽核負擔
- 沒有專門的形式驗證團隊
- 有可從外部 I/O 中分離的小型函式
目前限制事項
- 證明任意完整的 Go 應用程式
- 包含 DB、API、網路、UI 的整體處理
- 檢測所有安全漏洞
- 暫不支援的語法、外部依賴或規格不明確
FAQ
首次諮詢前常見問題
這裡彙總諮詢前常見的問題，包括可證明範圍、AI 的角色和程式碼處理方式。
能消除所有錯誤嗎？
不會。我們只在明確列出的假設、檢查範圍和支援的 Go 子集內檢查指定性質，並不保證整個應用程式或外部系統。
需要學習 Lean 或 Rocq 嗎？
首次審查不需要。我們先確認與外部 I/O 分離的 Go 策略函式，以及想保證的性質。
由 AI 判斷正確性嗎？
不會。Gemini 產生性質、證明策略和證明候選；最終憑證的接受或拒絕由 MPK 獨立核心完成。
如果無法完成證明會怎樣？
我們會將結果整理為反例、無法判定或超出範圍，並說明原因、所需規格、修正候選，以及如何切出可證明的單元。
可以整合到 CI/CD 嗎？
在證明可行性審查確認檢查範圍和可證明性後，可另行提出持續檢查或 CI/CD 整合方案。
諮詢時需要提交程式碼嗎？
無需在公開表單中貼上機密程式碼。諮詢後，我們會確認 NDA 和安全的共享方式。
諮詢
確認自有程式碼的證明可行性。
請告訴我們最需要避免的失敗情境，以及想審查的 Go 函式。無需在公開表單中貼上機密程式碼。
支援 NDA 與安全程式碼共享