Dana Edwards
Back to home

Case study

MPRD: Model Proposes, Rules Decide

Lets an AI agent act without letting it act unsafely. A model proposes, a deterministic gate decides, and the executor runs only what carries a valid, verified receipt.

Summary

MPRD is built around a simple control boundary. An untrusted model generates candidate actions. A deterministic rules layer issues the evidence required for execution. The model has no direct execution capability.

MPRD control boundary: a model proposes, a deterministic gate decides, and the executor acts only on a verified receipt. Untrusted model proposes candidate actions Deterministic gate policy + state + proof checks decide Executor acts only on a verified receipt proposes valid receipt Rejected: fail closed missing · tampered · stale · replayed
The control boundary: the model proposes, the gate decides, and the executor acts only on a verified receipt. Every admitted action carries policy, state, action, and receipt commitments; missing, tampered, stale, or replayed receipts fail closed.
MPRD operator UI: a decision audit log listing proposed actions with Allowed or Denied verdicts, a Verified proof status, and execution results.
The MPRD operator UI, running locally on mock data with no backend attached. Every proposed action is recorded with a verdict (Allowed or Denied), a proof status (Verified), and an execution result. The gate's decisions are the audit trail.
MPRD demonstrates architectural judgment: capability separation, typed execution boundaries, policy/state/action commitments, and fail-closed verifier behavior.

What a reviewer should inspect first

  1. README.md - high-level thesis and architecture.
  2. crates/mprd-core/ - core types and execution-boundary language.
  3. proofs/lean/ - proof artifacts and theorem surfaces.
  4. docs/RC1_BLOCKERS.md - honest remaining gaps before stronger release claims.
  5. docs/PRODUCTION_READINESS.md - implementation status and production-readiness posture.

Suggested 10-minute review script

Open the README, then inspect the core execution token / proof bundle types. Finally, read the blocker board before evaluating any high-level safety claim.

Claim / evidence map

ClaimEvidence to showStatus
Model output has no direct execution path in the architecture. Executor APIs should require verified token, receipt, or ready bundle inputs. Raw model output stays outside the execution API. Partial / architecture-level
Policy, state, candidate, and action commitments are part of the execution transcript. Core types, hashes, proof bundles, verifier checks, and tests. Partial / bounded
Production deployment is fully safe. Would require complete proof chain, deployment assumptions, operational controls, and external review. Not claimed

Limitations to state clearly

  • A formal gate is only as good as its policy, state provenance, implementation boundary, and deployment assumptions.
  • Architecture-level separation gives a bounded claim about the execution boundary.
  • Strong claims should be scoped to exact modes, exact toolchains, exact threat models, and exact replay/proof commands.

Open MPRD on GitHub