MPK Assurance / Go Proof Readiness Review

We prove
your Go code, not just test it.

We mechanically check critical Go logic that moves money, such as refunds, fees, balances, and reserves, against explicit specifications, assumptions, and scope. Gemini prepares proof candidates, and the independent MPK kernel makes the final verdict.

Try the 30-second refund demo Request a Proof Readiness Review

Limited to the First 5 Companies MPK Early Adoption Offer JPY 49,800(before tax)

Start with one Go function

Up to 2 properties

No public input of
confidential code

Deliver
re-checkable evidence

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 violates the property.

KERNEL VERIFIED

The kernel accepted the fixed canonical certificate.

Assurance Beyond TestingStart from ordinary GoSeparate AI from trust decisionsShow proof, counterexamples, and exclusions

30-second Refund Demo

Find a counterexample, then prove the fixed version.

Try the prepared refund code and see the flow from counterexample to fix to successful proof. You do not need to enter confidential code in the public demo.

Refund policy: cumulative refunds must not exceed the amount paid

Property to Verify

0 ≤ refunded + amount ≤ paid

Target: one refund policy function
Inputs: non-negative integers
External I/O, DB, and network are out of scope
Checked within explicit assumptions and a Go subset

Verification Result (buggy implementation)

Counterexample Found

We found concrete inputs where the cumulative refund exceeds the amount paid.

paid = 100
refunded = 80
amount = 30
result = 110 (property violation)

Technical Details

Run ID: run_refund_bug_20260727
Certificate hash: — not generated because a counterexample was found
Kernel verdict: REJECTED / COUNTEREXAMPLE
Axiom report: integer arithmetic / explicit assumptions

Result Classification

Four Result Types

Proved

The specified property holds under the explicit assumptions and scope.

PROVEN

Counterexample Found

We show concrete inputs that violate the property and clarify what condition needs to be fixed.

FALSIFIED

Unknown

We clearly report when the current strategy cannot determine whether the property holds.

UNKNOWN

Out of Scope

We explain specific reasons we cannot handle the target, such as unsupported syntax, external I/O, or unsupported behavior.

INAPPLICABLE

Difference from Testing

We check the specified property, not only selected inputs.

Testing (example-based)

Runs the cases you wrote
Leaves unselected inputs uncovered
A passing result is not a certificate
Trust depends on test design

MPK Assurance (Proof)

Checks specified properties and scope
Shows concrete inputs that break the property
Leaves a re-checkable certificate and hash
An independent kernel makes the final verdict

Comparison	Testing	Proof
Target	Selected inputs	Specified property
Counterexample display	△	○
Re-check	Execution log	Certificate
Final judgment	Test suite	Kernel

3 Features

Assurance Beyond Testing

We check the property against explicit specifications, assumptions, and scope, not just a few sample inputs.

Use Go, Not a Special Proof Language

You can start with a critical Go policy function isolated from external I/O.

Let AI Prove, But Do Not Trust AI

AI only prepares candidates. Final acceptance is performed by an independent kernel that reads the canonical certificate.

Let AI do the work. Do not let AI make the final judgment.

CustomerSubmit a Go function and the property to guarantee

GeminiPropose properties, strategy, and proof candidates

MPKTrust boundary that independently checks certificates

HumanConfirm specifications, assumptions, and confidentiality

EvidenceDeliver a re-checkable Evidence Pack

Gemini runs the proof workflow, MPK makes the trust decision, and a human approves the delivery.

Use Cases Where Verification Helps

RefundsCumulative refunds must not exceed the amount paid

FeesNever negative and never above contract caps

ReservesPost-processing balance does not fall below the minimum

DiscountsStays within limits even when discounts stack

PointsIssued points do not exceed the budget limit

DistributionDistributed amounts add up to the original principal

Evidence Pack

We deliver re-checkable evidence, not an AI answer.

FINITE FIELD

MPK CERTIFICATE

Proof Readiness Review
Canonical Certificate Record

KERNEL VERDICT
ACCEPTED

MPK

Certificate hash
MPK kernel verdict
Go reference checker result
Axiom report
Proved properties and stated assumptions
Excluded scope and out-of-scope reasons
Counterexample, if found
Run ID and re-check information

Proof Readiness Review

Review your first function within a fixed scope.

JPY 198,000 (before tax)

One Go function
Up to 2 properties to prove
Classifies results as proved, counterexample, unknown, or out of scope
Evidence Pack and an online walkthrough of the results

View the early adoption offer

This is the planned standard price. We are currently running an early adoption campaign limited to the first 5 companies at JPY 49,800 before tax.

MPK Early Adoption Offer

Limited to the First 5 Companies

Check whether your critical Go code can be proved, not just tested.

In the MPK Proof Readiness Review, we choose one target Go function, define the property to guarantee, generate proof candidates with AI, and run an independent check with the MPK kernel.

What is Included

One Go function
Up to 2 properties to prove
MPK compatibility assessment
A report on proofs, counterexamples, proof blockers, and out-of-scope items
A report summarizing the proof scope and assumptions

Campaign Conditions

This offer is for companies that can provide candid feedback after the service and approve a case study for publication on the MPK official site. The case study may include the company name, contact name, title, feedback, and either a representative photo or company logo.

Company NameNameTitleFeedbackRepresentative photo or company logo

You will review the content before publication, and we will use only approved material. We do not ask for a favorable review.

Service Flow

Service Flow (5 Steps)

Discovery

Confirm the failure scenario that could cause loss and the target function.

Scope Lock

Lock the function, property, assumptions, and excluded scope.

Gemini + MPK Review

AI prepares candidates, and MPK checks the certificate.

Results Walkthrough

Walk through the proof, counterexample, unknown result, exclusions, and evidence.

Next Steps

Clarify whether to move into fixes, additional functions, or CI/CD integration.

Best Fit

You implement refund, fee, or balance logic in Go
A single defect could cause financial loss or audit burden
You do not have a dedicated formal verification team
You have a small function that can be isolated from external I/O

Current Limitations

Proof of an arbitrary entire Go application
End-to-end processing that includes DB, APIs, network, or UI
Detection of every security vulnerability
Unsupported syntax, external dependencies, or unclear specifications

FAQ

FAQ Before the First Consultation

These answers cover common questions before you contact us, including proof scope, the role of AI, and how code is handled.

Does this eliminate all bugs?

No. We check the specified property only within the explicit assumptions, scope, and supported Go subset. This does not guarantee the entire application or external systems.

Do we need to learn Lean or Rocq?

Not for the first review. We start by confirming a Go policy function isolated from external I/O and the property you want to guarantee.

Does AI decide what is correct?

No. Gemini creates properties, proof strategies, and proof candidates. The independent MPK kernel accepts or rejects the final certificate.

What happens if proof fails?

We classify the result as a counterexample, unknown, or out of scope, then explain the reason, required specifications, likely fixes, and how to isolate a provable unit.

Can this be integrated into CI/CD?

After the Proof Readiness Review confirms the target and proof feasibility, we can separately propose continuous checks or CI/CD integration.

Do we need to send code with the inquiry?

You do not need to paste confidential code into the public form. After inquiry, we will confirm NDA handling and a secure sharing method.

Contact

Check whether your code can be proved.

Tell us which failure would matter most and which Go function you want reviewed. You do not need to paste confidential code into the public form.

NDA and secure code sharing supported

Company Name

Name

Work Email Address

Target Logic

Which failure would matter most?

Request an NDA

Do not enter source code, credentials, or personal data in the public form.

Preview submission received. On the production site, connect this to the existing inquiry flow.