-
-
MPK turns Go policy code into a canonical proof certificate, verifies it with a Rust kernel, and produces portable evidence.
-
go2gir analyzes a Go policy, creates a canonical proof certificate, and sends it to the Rust MPK kernel for verification.
-
AI output, source code, and passing tests are useful—but they do not prove a payment policy is safe. MPK adds checkable evidence.
-
The same proof certificate is independently checked by Rust MPK and the Go reference checker, with matching accepted results.
-
An actual MPK run verifying a proof certificate and returning an accepted result with certificate-linked output.
Inspiration
AI can now write code, review pull requests, and recommend operational decisions at a remarkable pace. That speed is useful, but it creates a serious problem for high-impact workflows: a convincing explanation is not the same thing as a verifiable guarantee.
We were especially concerned about small teams using AI to change payment, reserve, approval, and access-control policies. A seemingly minor implementation error can approve an amount that should be blocked, bypass a required review, or silently alter a financial rule. Existing AI coding workflows often rely on source code, test results, model output, and CI status. All of those are useful, but none of them is sufficient evidence that a critical policy is correct.
MPK ProofOps is built around a different question: can an AI-assisted workflow produce a compact proof artifact that anyone can independently check, even without trusting the AI, the original source code, or the system that generated the proof?
What it does
MPK is a machine proof kernel and verification toolchain. It checks canonical proof certificates through a small trusted Rust kernel and can validate the same certificate through an independent source-free reference checker.
For the ProofOps path, MPK focuses on restricted Go payment-policy functions. An untrusted frontend translates supported Go code into an intermediate representation and generates verification conditions. The trusted kernel never accepts that source code, the generated conditions, a solver response, or an AI explanation as proof. It accepts only a canonical certificate that passes kernel checking.
The result is structured, deterministic evidence for a policy decision. This includes the certificate hash, exported artifact hash, theory-certificate information, and an axiom report. A product can present this evidence to an operator, auditor, or customer, while preserving a clear distinction between verified facts and helpful but untrusted analysis.
For example, a team can use MPK to verify a bounded payment reserve rule in a Go service. The policy workflow produces either a verified evidence record or a fail-closed result that clearly states why verification was not established.
How we built it
We built MPK as a Rust workspace with deliberately narrow trust boundaries. The core implements terms, type checking, reduction, definitional equality, declarations, and inductive constructs. The certificate layer provides canonical encoding, decoding, imports, exports, hashing, and axiom reporting. The kernel orchestrates fast certificate verification and emits structured results.
We also built a separate Go reference checker that can verify proof certificates without source code. This is important because independent checking reduces reliance on a single implementation path.
The Go frontend is intentionally outside the trusted computing base. It uses Go analysis tooling to inspect a restricted language subset and emits deterministic intermediate artifacts. Unsupported language features are rejected instead of being guessed at. Verification-condition generation, contracts, AI outputs, solver outputs, Markdown reports, and CI results remain helper artifacts; they may guide a user, but they do not become proof evidence.
The command-line workflow supports certificate checks, package verification, axiom reports, policy scans, and policy verification. It is designed so that a customer-facing product can consume machine-readable evidence without weakening the kernel's security model.
What we learned
The key lesson was that “AI-assisted” and “verifiable” are not automatically compatible. AI is valuable for proposing code, contracts, and explanations, but critical acceptance decisions need a much smaller and more auditable trust base.
We also learned that provenance matters as much as a pass/fail label. A verified claim should identify exactly which certificate was checked, which theory assumptions were used, and whether any axioms were admitted. This makes the evidence portable across CI systems, dashboards, and independent checkers.
Another lesson was that practical verification requires disciplined scope. Rather than claiming to prove arbitrary programs, MPK starts with a restricted, fail-closed subset where the verification boundary is explicit and reviewable.
Challenges ahead
The hardest engineering challenge is maintaining a useful developer workflow without expanding the trusted base. Source parsing, contract extraction, verification-condition generation, solvers, and AI agents are all productive components, but they must remain non-authoritative.
A second challenge is broadening supported policy patterns while preserving deterministic artifacts and independent verification. We are addressing this through versioned schemas, checked theory certificates, explicit axiom reports, and a strict separation between trusted proof evidence and product-side analysis.
MPK ProofOps is the verification engine for a future AI-native policy operations product: AI can help teams move faster, while the final safety claim remains something that can be checked rather than merely believed.
Log in or sign up for Devpost to join the conversation.