Skip to content

Proof-Carrying Artifact Gate

Acceptance protocol — instantiates Generate-and-Verify Separation

Admits an artifact across a trust boundary only if it arrives bundled with a machine-checkable proof that it satisfies the consumer's stated policy — so the producer can be wholly untrusted.

Proof-Carrying Artifact Gate flips the burden of trust at the point of acceptance. Instead of the consumer inspecting or re-deriving an incoming artifact, the consumer publishes a policy and demands that every artifact carry its own proof of complying with it. The gate's job is narrow and mechanical: confirm the attached certificate is well-formed, that it establishes the stated policy, and that it is bound to this artifact — then admit or reject. Its defining move, versus a checker that re-does the producer's work, is that the expensive obligation (constructing the proof) is pushed onto the producer while the consumer keeps only the cheap obligation (checking it). It is the Proof-Carrying Code idea generalised to any artifact that can ship with evidence.

Example

A platform lets third parties ship native, performance-critical modules that run inside its trust boundary. Rather than hand-audit each submission or sandbox away the performance, the platform defines a memory-safety policy and requires every module to arrive with a proof that its machine code obeys that policy. When a vendor uploads a module, the gate checks three things: the proof is syntactically valid, it establishes exactly the platform's policy (not a weaker one), and its hash binds it to the uploaded binary rather than some other build. A module whose proof checks is admitted with no human in the loop; one whose proof is missing, malformed, or proves the wrong property is turned away at the door. The vendor's compiler can be proprietary and untrusted — the platform trusts only its own small proof-checker and the policy it wrote.

How it works

  • Publish the policy, not a review. The consumer states the acceptance property once, in checkable form; that statement is the contract every producer codes against.
  • Require evidence to travel with the artifact. Submissions are refused unless they carry a certificate in the agreed format — no certificate, no consideration.
  • Check the proof, not the producer. The gate validates the certificate against the artifact and the policy; it never re-runs the producer's search or leans on reputation.
  • Bind, then gate. Acceptance requires the certificate to be structurally or cryptographically tied to the exact artifact, after which the release gate admits it.

Tuning parameters

  • Policy strength — how much the proof must establish (memory safety only vs. full functional correctness). Stronger policies admit less bad code but make proofs harder to produce, shrinking the pool of producers who can comply.
  • Certificate format — the proof language producers must target. A more expressive format eases proof construction but enlarges the checker; a restricted one keeps the gate tiny.
  • Binding method — how tightly the certificate is tied to the artifact (content hash, signature, embedding). Looser binding is convenient but invites proof-reuse or swap attacks.
  • Gate placement — where the check runs (submission, install, or load time). Later gates catch tampering in transit but cost latency on every use.

When it helps, and when it misleads

Its strength is that a consumer can safely accept artifacts from many untrusted, even anonymous, producers at scale, because acceptance cost is fixed and small while production cost is borne by whoever wants in. It also makes the acceptance criterion explicit and uniform — everyone is held to the same published policy.[1]

Its failure modes turn on the gap between policy and intent. The gate certifies the policy, not your purpose: an artifact can carry a flawless proof of a policy that fails to capture what you actually needed — a proof of memory safety says nothing about a memory-safe module that exfiltrates data. A bug in the checker or the proof format admits forged certificates. And the gate is run backwards when a team weakens the policy until the artifacts they already wanted to ship happen to pass. The discipline is to treat the policy as the real security decision — reviewed and versioned as carefully as code — and to keep the checker and its trusted format small enough to audit.

How it implements the components

  • witness_or_certificate_contract — defines the proof the artifact must carry and in what format; the gate consumes exactly this.
  • candidate_claim_contract — the artifact declares which policy it claims to satisfy, the claim the proof must then establish.
  • verification_scope_statement — the published policy fixes precisely what "acceptable" means and, by omission, what the gate does not check.
  • verdict_and_release_gate — the pass/fail decision that admits the artifact across the trust boundary or refuses it.

It does not itself re-derive proofs from primitives or hold the soundness kernel (trusted_verifier_kernel, checkable_acceptance_predicate) — that engine is Proof-Assistant Kernel Check — nor shrink the proof cryptographically or hide the witness (privacy_and_disclosure_boundary, generation_verification_cost_model), which is Succinct Cryptographic Proof Verifier.

Notes

The gate is a transport-and-decision wrapper; it presupposes the acceptance property is expressible as a checkable predicate and that a real checker exists to run underneath it (which it consumes). Artifacts whose desired property resists formalization cannot be gated this way and fall back to review — the gate moves when the assurance work happens, not whether it is possible.

References

[1] Proof-Carrying Code (Necula & Lee, 1990s): untrusted native code ships with a machine-checkable proof of a safety policy, which the host validates before execution. The gate here generalises that producer-proves / consumer-checks split to any artifact that can carry evidence. ↩