SZL Holdings · Doctrine v11 · Λ = Conjecture 1 (advisory, never "green"/theorem) · canonical a-11-oy.com

szl-receipt

Control before action. Evidence after.

Part of the szl-holdings estate · Product: a-11-oy.com · Proof: a11oy.net

Shared signed-receipt library for SZL components. Provides cryptographically signed per-inference receipts using DSSE/ECDSA-P256-SHA256 (cosign-compatible), with an UNSIGNED-honest fallback when no signing key is present.

Built on pinned, maintained libraries — no hand-rolled DSSE/crypto: in-toto-attestation 0.9.3 (ITE-6 Statement/predicate bindings) for attestation construction and cryptography 50.0.1 for the ECDSA P-256 signature primitive. The DSSE PAE is the spec encoding (ASCII decimal lengths over the decoded payload bytes), byte-for-byte compatible with cosign verify-blob.

Install

pip install szl-receipt

Or from source:

pip install -e ".[dev]"

Quick start

from szl_receipt import Receipt, sign_receipt, verify_receipt, generate_keypair, PAYLOAD_TYPE

# 1. Build a receipt
r = Receipt(kind="inference", body={"model": "gpt-4o", "policy": "allow", "score": 0.99})
digest = r.digest()  # SHA-256 hex over canonical_json(body)

# 2a. Keyless — UNSIGNED-honest
env = sign_receipt(r, private_key_pem=None, organ="a11oy")
# env["signed"] == False, env["note"] == "UNSIGNED-honest: no cosign key present"

ok, detail = verify_receipt(env)           # -> (False, "unsigned-honest") — NEVER a fake pass

# 2b. Signed — DSSE/ECDSA-P256-SHA256
priv_pem, pub_pem = generate_keypair()
env2 = sign_receipt(r, private_key_pem=priv_pem, organ="a11oy")

ok, detail = verify_receipt(env2, public_key_pem=pub_pem)   # -> (True, "ok")

Envelope schema

verify_statement validates the complete statement structure and every subject digest mapping before checking the caller's expected digest. Malformed statements return False; digest algorithm labels and values must be non-empty strings and are never coerced. Every subject needs a non-empty name, matching the existing SZL builder contract. Present optional descriptor fields must have valid types, content must be base64, and predicate/subject values must be finite JSON data. Unknown descriptor extensions remain accepted. Structural failures return invalid-statement-structure, including missing subjects. Success checks structure and digest binding only: signature verification, signer trust, and authorization remain separate. An unsigned receipt still returns unsigned-honest from verify_receipt.

The run-manifest emitter requires a JSON object with exact boolean heldout_passed and refusal_no_regression verdicts and a finite numeric pass_rate in [0, 1] (booleans are not rates). Duplicate JSON members are rejected. Invalid evidence fails before output is written; valid negative verdicts stay negative, and signature/conformance declarations retain their existing false defaults.

Field	Type	Description
payloadType	str	DSSE payload type URI
payload	str	base64(canonical_json(body))
signature	str	base64(DER ECDSA-P256 sig), "" when unsigned
signed	bool	True when real signature present
organ	str	Signing authority label
keyid	str	Optional key identifier
digest	str	SHA-256 hex of canonical_json(body)
algo	str	"ECDSA-P256-SHA256" or "UNSIGNED"
note	str	Present only when unsigned; value: "UNSIGNED-honest: no cosign key present"

cosign verification

Save the public key as organ.pub, then:

cosign verify-blob --key organ.pub \
    --payload <(echo -n "$payload_b64" | base64 -d) \
    --signature <(echo -n "$sig_b64" | base64 -d)

Crypto doctrine

• UNSIGNED-honest: no key → signed=False, signature="", and verify_receipt returns (False, "unsigned-honest") — NEVER a fake pass.
• One canonical hash: SHA-256 over canonical_json(body) (sorted keys, compact separators, UTF-8). Resolves SHA3-vs-SHA256 drift.
• cosign-compatible: the PAE is the DSSE-v1 spec encoding — DSSEv1 SP LEN(type) SP type SP LEN(body) SP body with ASCII decimal lengths over the decoded payload bytes — byte-for-byte compatible with cosign verify-blob. (Pre-migration releases used a non-standard binary-length PAE whose cosign compatibility claim was false; receipts signed before 0.4 must be re-issued.)
• Pinned maintained libraries: attestation statements are constructed and validated through in-toto-attestation 0.9.3; signatures are ECDSA P-256 via cryptography 50.0.1. No hand-rolled DSSE or crypto primitives.

GovernedAction v1: one release truth, not six disconnected greens

szl-receipt 0.3 adds a fail-closed, multi-subject release attestation using the https://szl.dev/GovernedAction/v1 predicate. One standard DSSE envelope binds all seven required subjects:

• GitHub source revision
• Hugging Face repository revision
• runtime artifact digest
• provider deployment digest
• domain-state evidence
• durable receipt identity
• independent runtime witness

The signed predicate also binds the authenticated actor, evaluated policy, evidence obligations, side effects, timestamps, evidence sources, and freshness bounds. verify_governed_action independently recomputes the result. Missing, stale, duplicate, contradictory, malformed, unsigned, or unverifiable evidence returns INCOMPLETE; the producer's embedded assessment is never trusted.

from szl_receipt import emit_governed_action, verify_governed_action

envelope = emit_governed_action(
    action=action,
    actor=actor,
    policy=policy,
    subjects=subjects,
    subject_roles=subject_roles,
    evidence=evidence,
    obligations=obligations,
    side_effects=side_effects,
    assessed_at="2026-08-13T12:00:00Z",
    private_key_pem=private_key_pem,
)
result = verify_governed_action(envelope, public_key_pem)
assert result.status in {"PASS", "INCOMPLETE"}

The API performs no network, provider, deployment, or filesystem mutation. The caller supplies observed evidence; the verifier decides whether those exact bytes form a fresh, internally consistent, signed admission record.

Proof-Carrying Inference (PCI)

PCI is a receipt profile layered on the PCGI spine. Where PCGI binds model + input + output + policy + energy (+ BFT witnesses), PCI adds the two bindings that make a governed decision offline-verifiable as a governance warrant — a receipt R = ⟨π, τ, ε, (Λ ≥ θ, σ)⟩:

Field	Binding	Backing kernel
π	provenance / DSSE envelope + in-toto statement	szl-receipt (this repo)
τ	confidential-execution attestation (○ specified; roadmap)	—
ε	measured energy, joules verbatim or UNAVAILABLE	szl-energy-attest
Λ ≥ θ	non-compensatory roll-up Λ = Π xᵢ^wᵢ, re-computed on verify	szl-lambda-gate
σ	machine-checked spec reference + tier guard	lutar-lean (locked tier)

Both PCI bindings ride inside the sanctioned PCGI extra extension point, so they are part of the signed body digest — tamper-evident — without forking the spine. verify_pci_receipt first runs the existing spine verifier, then recomputes Λ from the bound scores (a wrong Λ is caught offline, not merely asserted) and enforces the tier guard.

from szl_receipt import generate_keypair, lambda_gate as lg
from szl_receipt.pci import SpecRef, emit_pci_receipt, verify_pci_receipt

verdict = lg.evaluate(
    scores={"safety": 0.96, "provenance": 0.90},
    weights={"safety": 0.5, "provenance": 0.5},
    theta=0.80,
)                                              # Λ = weighted geometric mean

priv, pub = generate_keypair()
r = emit_pci_receipt(
    model_id="szl-router/llama-3.1-8b",
    input_digest="sha256:in…", output_digest="sha256:out…",
    policy_id="tcpa-compliance.v11",
    lambda_verdict=verdict, spec=SpecRef(), energy_joules=12.5,
    organ="a11oy", private_key_pem=priv,
)

res = verify_pci_receipt(r, public_key_pem=pub, require_measured_energy=True)
# res.ok is True, res.advisory == "advisory-pass", res.energy == "MEASURED"

Runnable end-to-end demo: examples/proof_carrying_inference.py.

PCI honesty doctrine (never weakened)

• Λ is advisory. A pass clears a non-compensatory threshold — it is not a proof of correctness, safety, or conformity.
• Λ recomputed, not trusted. The verifier recomputes Λ = Π xᵢ^wᵢ from the bound scores; a producer's wrong Λ fails offline (lambda-recompute-mismatch). Emission also rechecks the bound verdict, including hand-built verdicts and scores mutated after evaluation. Malformed score containers and integers too large for a float are refused with a reason during verification. Every bound score is validated before the zero veto, so a zeroed axis never masks an invalid one (lambda-invalid:…).
• θ lies in (0, 1]. θ = 0 would pass a zero-vetoed Λ (0 ≥ 0), so lambda_gate.evaluate refuses it and the verifier refuses a bound θ outside (0, 1], NaN or ∞ included (theta-invalid:…).
• Tier guard refuses overclaims — by allowlist, not denylist. Spec claims are validated against a fixed allowlist of honest tokens, so no overclaim survives however it is reworded. The specific machine-checked non-theorems — unconditional Λ-uniqueness (Conjecture 1, false as stated → overclaim-conjecture1) and unconditional Khipu BFT safety (Conjecture 2, open → overclaim-conjecture2) — are refused with their exact reason code, scanned across claims and invariants. Λ-uniqueness is conditional (Theorem U). locked_count is derived from the invariant list so it cannot drift.
• Energy is measured-or-UNAVAILABLE. require_measured_energy=True refuses a receipt lacking a real joule reading, and a non-finite joules value is refused as energy-malformed — a joule is never fabricated.
• Attestation (τ) is honest-only. Confidential-execution verification is not yet implemented, so only the UNAVAILABLE placeholder passes; a receipt asserting a "verified" enclave we cannot check is refused (attestation-unverifiable).
• Keyless stays UNSIGNED-honest — verify_pci_receipt returns unsigned-honest, never a fake pass.

Prior art (cited, not claimed as ours)

• G. Necula, Proof-Carrying Code, POPL 1997, doi:10.1145/263699.263712.
• Kol, Ben-Shahar, Sulimany, Englund, A machine-verified proof of a quantum-optimization conjecture, arXiv:2606.29687 (2026) — LLM proposes / Lean 4 certifies, the loop SZL points at governance rather than pure mathematics.
• SZL corpus concept DOI: 10.5281/zenodo.19944926.

Development

pip install -e ".[dev]"
pytest -q

SPDX

SPDX-License-Identifier: Apache-2.0
ORCID: 0009-0001-0110-4173

---

Explore the SZL estate: a11oy console · LLM Router · Receipt format spec · Lean proofs · Docs · 🤗 SZLHOLDINGS

_{The SZL Router signs every answer with this library, emitting the open governed-receipt-spec format.}