Skip to main content
When Guard.verify(...) returns allowed=True, it attaches a VerifiedCertificate to the result. The certificate is the audit-trail unit: it records what was verified, when, and by which prover.

​
Shape

The VerifiedCertificate dataclass lives in agentsafe/kernel/certificate.py. Its fields:
FieldTypeMeaning
idstr (uuid)Unique certificate id.
theoremstrIdentifier of the theorem-like obligation Z3 discharged for this call.
plan_hashstrSHA-256 of the plan / call structure being verified.
verified_propertieslist[str]The properties Z3 confirmed (e.g. capability_coverage, budget_sufficient).
proof_tracestrFree-form trace of the Z3 solve, used for audit reproducibility.
proverstrThe prover that issued the certificate. Default "z3".
issued_atfloatUnix epoch seconds at issue time.
expires_atfloat | NoneOptional expiry, set when the call carries a TTL.
_signaturestrHMAC-style signature bound to the kernel-issued signing key.

​
How to inspect one

result = guard.verify(
    tool="web_fetch",
    required_capabilities=["network:http:read"],
    cost_cents=10,
)

if result.allowed and result.certificate is not None:
    cert = result.certificate
    print(cert.id)                   # e.g. "8c5e...-d4a1"
    print(cert.theorem)              # the obligation that was discharged
    print(cert.verified_properties)  # ["capability_coverage", "budget_sufficient", ...]
    print(cert.prover)               # "z3"

​
The Lean policy fingerprint

Every certificate is implicitly bound to the policy model the runtime enforces. The fingerprint is the short SHA-256 of the Lean source under lean4/CertiorLattice/Certior/, computed by certior.guard._lean_policy_fingerprint() at runtime and woven into the certificate in three places:
  • as part of the JSON that produces plan_hash (so tampering with the recorded action invalidates the receipt),
  • in verified_properties as a string of the form "policy_model:lean-audited@<fingerprint>",
  • in proof_trace as "Z3 SAT in <ms>ms, policy: Lean-audited @ <fingerprint>".
Query the fingerprint from your installed package: 
from certior.guard import _lean_policy_fingerprint
print(_lean_policy_fingerprint())   # e.g. "cc3e0c7431fd8a53"
The value changes whenever the Lean source changes. An auditor reproduces the audit by:
  1. Cloning the repository at the commit referenced in the certificate’s plan_hash.
  2. Running lake build Certior.Audit in lean4/CertiorLattice/.
  3. Recomputing the fingerprint from the cloned Lean source and confirming it matches the value embedded in verified_properties and proof_trace.
  4. Confirming the four headline theorems still depend only on Lean’s three standard axioms.
If any of these fails, the certificate’s claim to “verified by the same policy model” is invalid.

​
Where certificates live

  • The full VerifiedCertificate (with signature) lives on the returned VerifyResult.certificate.
  • Guard.audit_log keeps a lightweight metadata trail per call: {tool, allowed, violations: int, pii_count: int, latency_ms, time}. It does not carry the certificate or the violations list - those are on the return value.
  • Optional persistent store: when running with the FastAPI server, certificates are persisted per execution and can be exported via GET /api/v1/compliance/{execution_id}/export.

​
See also