Documentation
¶
Overview ¶
Command proof-carrying-run is a worked example of a PROOF-CARRYING RUN: a run that ships a single, offline-checkable certificate asserting behavioral-property compliance over the whole run, checked against one signed tree head. It composes existing audit primitives (anchored policy and convergence leaves, the policy-used absence commitment, RFC 6962 inclusion proofs, a signed tree head) into one per-run certificate plus a verifier; there is no new cryptography.
The example is offline: no LLM, no network. The "agent" applies governed actions through govern.AttestedEventTool (each journaled with the policy digest that admitted it), exactly as a real agent loop would; the governed guarantees are identical. It:
- anchors a convergent policy and its convergence certificate, runs governed actions under it;
- emits a RunCertificate asserting only-approved-policies and policies-convergence-certified;
- verifies the certificate offline against the public key alone (PASS);
- shows the FAIL path: with the SAME certificate but a narrower approved allowlist (as if a disallowed policy had been used), only-approved-policies fails and the completeness commitment has teeth: dropping the used policy from the disclosed set breaks the signed absence root too.
What the certificate proves, precisely: properties of the GOVERNED, COMMITTED boundary (which policies ran, that each is approved and has an anchored, oracle-checkable convergence certificate). It does NOT prove the model's judgment was correct or close the runtime-refinement gap.
Source Files