要验证的性质（Property）
0 ≤ refunded + amount ≤ paid
- 对象：1 个退款策略函数
- 输入：非负整数
- 外部 I/O、DB、网络不在检查范围内
- 在明确列出的假设和 Go 子集内检查
MPK Assurance / Go Proof Readiness Review
我们不只是测试，
而是证明你的 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
}PROPERTY (TO VERIFY)
∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid
COUNTEREXAMPLE FOUND
paid=100, refunded=80, amount=30 违反性质。
KERNEL VERIFIED
内核已接受修正版 canonical 证书。
超越测试的保证从日常 Go 开始将 AI 与信任判断分离明确证明、反例和超出范围
30 秒退款演示
发现反例，并证明修正版。
可使用预置的退款代码体验“反例 → 修正 → 证明成功”的流程。无需在公开演示中输入机密代码。
退款策略：累计退款额不得超过已支付金额
验证结果 （有 bug 的实现）
发现反例
发现了累计退款额超过已支付金额的具体输入。
paid = 100
refunded = 80
amount = 30
result = 110（性质违反）
refunded = 80
amount = 30
result = 110（性质违反）
技术详情
- Run ID
- run_refund_bug_20260727
- Certificate hash
- —（因反例未生成）
- Kernel verdict
- REJECTED / COUNTEREXAMPLE
- Axiom report
- integer arithmetic / explicit assumptions
Result Classification
结果分为 4 类
已证明
指定性质在明确的假设和检查范围内成立。
PROVEN发现反例
展示破坏性质的具体输入，并明确需要修正的条件。
FALSIFIED证明未完成
明确报告当前策略无法确定成立或不成立的状态。
UNKNOWN超出范围
具体说明无法处理的原因，例如暂不支持的语法、外部 I/O 或功能限制。
INAPPLICABLE与测试的区别
检查指定性质，而不只是少量选定输入。
测试（示例式）
- 执行写好的用例
- 未覆盖的输入仍然存在
- 测试通过并不等于证明证书
- 信任依赖测试设计
MPK Assurance（证明）
- 检查指定性质及范围
- 具体展示破坏性质的输入
- 留下可复查的证书和 hash
- 独立内核做最终判定
| 比较 | 测试 | 证明 |
|---|---|---|
| 对象 | 选中输入 | 指定性质 |
| 反例显示 | △ | ○ |
| 复查 | 执行日志 | 证书 |
| 最终判断 | 测试体系 | 内核 |
3 个特点
超越测试的保证
不是只跑少量示例输入，而是在明确的规格、假设和检查范围内检查性质。
使用 Go，而不是特殊证明语言
可以从与外部 I/O 分离的关键 Go 策略函数开始。
让 AI 证明，但不信任 AI
AI 只负责生成候选。最终是否接受，由读取 canonical 证书的独立内核决定。
让 AI 工作，但不让 AI 做最终判断。
客户提交 Go 函数和想保证的性质
Gemini提出性质、策略和证明候选
MPK独立检查证书的信任边界
人确认规格、假设和机密性
证据交付可复查的 Evidence Pack
Gemini 运行证明流程，MPK 做信任判定，由人确认后交付。
适合验证的用例
退款累计退款额不得超过支付金额
手续费不为负，且不超过合同上限
预留金处理后余额不低于最低额
折扣多个折扣叠加也不超过上限
积分发行量不超过预算上限
分配分配总额与原始金额一致
Evidence Pack
交付的是可复查的证据，而不是 AI 的回答。
FINITE FIELD
MPK CERTIFICATE
Proof Readiness Review
Canonical Certificate Record
KERNEL VERDICT
ACCEPTED
ACCEPTED
MPK
- Certificate hash
- MPK kernel verdict
- Go reference checker result
- Axiom report
- 已证明的性质与明确列出的假设
- 排除范围与超出范围原因
- 反例（如发现）
- 运行 ID 与复查信息
Proof Readiness Review
在固定范围内评审第一个函数。
198,000日元 （不含税）
- 1 个 Go 函数
- 最多 2 项待证明性质
- 将结果归类为已证明、发现反例、未能确定或超出范围
- Evidence Pack 与在线结果讲解
这是计划中的标准价格。目前正在开展前 5 家企业限定、49,800 日元（不含税）的早期采用优惠。
MPK 早期采用优惠
前 5 家企业限定确认贵公司的关键 Go 代码 是否能 不止通过测试，还能被证明。
在 MPK Proof Readiness Review 中，我们选择一个目标 Go 函数，整理要保证的性质，由 AI 生成证明候选，再由 MPK 内核独立检查。
服务内容
- 1 个 Go 函数
- 最多 2 项待证明性质
- MPK 适配性诊断
- 说明证明结果、反例、证明障碍或超出范围原因
- 汇总证明范围与假设的报告
优惠适用条件
本优惠面向愿意在服务完成后提供真实反馈，并批准在 MPK 官方网站发布案例的企业。案例内容可包括公司名称、姓名、职位、反馈，以及负责人照片或公司标志。
公司名称姓名职位反馈负责人照片或公司标志
所有发布内容都会在公开前请您确认，只使用已获批准的内容。我们不会要求好评。
Service Flow
服务流程（5 步）
需求确认
确认可能造成损失的故障场景和目标函数。
确定范围
锁定函数、性质、假设和排除范围。
Gemini + MPK 评审
AI 生成候选，MPK 检查证书。
结果说明
讲解证明、反例、未能确定、排除项和证据。
下一步建议
明确后续是否进入修正、更多函数或 CI/CD 集成。
适合以下企业
- 使用 Go 实现退款、手续费或余额逻辑
- 一个缺陷就可能带来资金损失或审计负担
- 没有专门的形式化验证团队
- 有可从外部 I/O 中切出的较小函数
当前限制事项
- 证明任意完整的 Go 应用
- 包含 DB、API、网络、UI 的整体处理
- 检测所有安全漏洞
- 暂不支持的语法、外部依赖或不明确规格
FAQ
首次咨询前常见问题
这里汇总咨询前常见的问题，包括可证明范围、AI 的角色和代码处理方式。
能消除所有 bug 吗？
不会。我们只在明确列出的假设、检查范围和支持的 Go 子集内检查指定性质，并不保证整个应用或外部系统。
需要学习 Lean 或 Rocq 吗？
首次评审不需要。我们先确认与外部 I/O 分离的 Go 策略函数，以及想保证的性质。
由 AI 判断正确性吗？
不会。Gemini 生成性质、证明策略和证明候选；最终证书的接受或拒绝由 MPK 独立内核完成。
如果无法完成证明会怎样？
我们会将结果整理为反例、证明未完成或超出范围，并说明原因、所需规格、修正候选，以及如何切出可证明的部分。
可以集成到 CI/CD 吗？
在 Proof Readiness Review 确认检查范围和证明可行性后，可另行提出持续检查或 CI/CD 集成方案。
咨询时需要提交代码吗？
无需在公开表单中粘贴机密代码。咨询后，我们会确认 NDA 和安全共享方式。
咨询
确认自有代码的证明可行性。
请告诉我们最需要避免的故障类型，以及想评审的 Go 函数。无需在公开表单中粘贴机密代码。
支持 NDA 与安全代码共享