検証する性質（Property）
0 ≤ refunded + amount ≤ paid
- 対象：1つの返金ポリシー関数
- 入力：非負の整数
- 外部I/O・DB・ネットワークは対象外
- 明示した仮定とGoサブセット内で検査
MPK Assurance / Go Proof Readiness Review
あなたのGoコードを、
テストではなく証明します。
返金・手数料・残高・リザーブなど、金銭を動かす重要なGoロジックを、明示した仕様・仮定・対象範囲で機械検査。Geminiが証明候補を作り、MPKの独立カーネルが最終判定します。
先着5社限定 MPK先行導入キャンペーン 49,800円（税別）Go関数1個から
性質最大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秒返金デモ
反例を見つけ、修正版を証明する。
用意済みの返金コードで「反例 → 修正 → 証明成功」を体験できます。公開デモに機密コードを入力する必要はありません。
返金ポリシー：累積返金額が支払済み金額を超えない
検証結果 （バグのある実装）
反例が見つかりました
累積返金額が支払済み金額を超える具体的な入力が見つかりました。
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
最初の1関数を固定スコープで診断します。
198,000円 （税別）
- Go関数 1個
- 証明したい性質 最大2件
- 証明・反例・証明未完了・対象外を分類
- Evidence Packとオンライン結果説明
通常提供予定価格です。現在、先着5社限定で49,800円（税別）の先行導入キャンペーンを実施しています。
MPK先行導入キャンペーン
先着5社限定自社の重要なGoコードを、テストするだけでなく、証明できるか確認してみませんか。
MPK Proof Readiness Reviewでは、対象となるGo関数を一つ選び、保証したい性質を整理したうえで、AIによる証明候補の生成とMPKカーネルによる独立検査を行います。
サービス内容
- Go関数1個
- 証明したい性質は最大2個
- MPK対応可否の診断
- 証明、反例、証明上の課題または対象外理由の報告
- 証明範囲と仮定をまとめたレポート
キャンペーン適用条件
サービス完了後、率直なご感想をご提供いただき、会社名、お名前、役職、ご感想、担当者写真または会社ロゴを、MPK公式サイトの導入事例として掲載することにご協力いただける方が対象です。
会社名お名前役職ご感想担当者写真または会社ロゴ
掲載内容は公開前にご確認いただき、承認を得た内容のみを使用します。好意的な評価をお願いするものではありません。
Service Flow
サービスの流れ（5ステップ）
ヒアリング
損失につながる失敗と対象関数を確認します。
スコープ確定
関数、性質、仮定、非対象範囲を固定します。
Gemini＋MPKレビュー
AIが候補を作り、MPKが証明書を検査します。
結果説明
証明、反例、未完了、対象外と証拠を説明します。
次段階の提案
修正、複数関数、CI/CDへの展開可否を整理します。
こんな企業に最適です
- Goで返金・手数料・残高ロジックを実装している
- 1件の不具合が金銭損失や監査負担につながる
- 形式検証の専任チームを持っていない
- 外部I/Oから切り離せる小さな関数がある
現在の制限事項
- 任意のGoアプリケーション全体の証明
- DB、API、ネットワーク、UIを含む処理全体
- すべてのセキュリティ脆弱性の検出
- 未対応構文・外部依存・不明確な仕様
FAQ
初回相談前によくある質問
証明できる範囲、AIの役割、コードの扱いなど、問い合わせ前に確認される内容をまとめています。
すべてのバグがなくなることを保証しますか？
いいえ。指定した性質について、明示した仮定、対象範囲、対応するGoサブセットの中で検査します。アプリケーション全体や外部システムまでを保証するものではありません。
LeanやRocqを学ぶ必要はありますか？
最初のレビューでは必要ありません。外部I/Oから切り離したGoポリシー関数と、保証したい性質を確認して開始します。
AIが正しいと判断するのですか？
いいえ。Geminiは性質や証明戦略、証明候補を作ります。最終的な証明書の受理・拒否はMPKの独立カーネルが行います。
証明できなかった場合はどうなりますか？
反例、証明未完了、対象外のいずれかとして理由を整理し、必要な仕様、修正候補、証明可能な切り出し方を説明します。
CI/CDへ導入できますか？
Proof Readiness Reviewで対象と証明可能性を確認した後、継続検査やCI/CDへの導入を別途提案します。
問い合わせ時にコードを送る必要がありますか？
公開フォームへ機密コードを貼る必要はありません。問い合わせ後、NDAや安全な共有方法を確認します。
お問い合わせ
自社コードの証明可能性を確認する。
発生すると最も困る不具合と、対象にしたいGo関数を教えてください。公開フォームに機密コードを貼る必要はありません。
NDA・安全なコード共有に対応