待验证性质
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 与安全代码共享