Stephen P. Lutar Jr.

Founder & CEO, SZL Holdings — cryptographic proof infrastructure for consequential AI decisions

$$\Lambda(x) ;=; \sum_{i=1}^{13} w_i,\phi_i(x), \qquad \sum_{i=1}^{13} w_i = 1,\quad w_i \ge 0, \qquad \texttt{receipts.in} \equiv \texttt{receipts.out}$$

-- machine-checked in lutar-lean@main
theorem lambda_bounded (x : ReceiptBus) : ‖Λ x‖ ≤ 1 := by
  simpa using isBounded_lambda x   -- A4 : IsBounded

I started SZL Holdings with one conviction: AI is moving into consequential decisions before the field has a proof layer.

Defense, healthcare, finance — operators are deploying AI that affects real outcomes, with no standard way to show what it decided, why, and whether it stayed within authorized parameters. Logs exist. Dashboards exist. Cryptographic proof does not.

The entire SZL stack is a machine for producing that proof — a DSSE-enveloped, hash-linked Khipu receipt that any auditor can verify on their own hardware, using public tooling, after the fact. The math is pinned in Lean 4. The supply chain is SLSA Build L2 verified. The shipping artifact is a signed UDS bundle deployable into any air-gapped cluster in one command.

I publish the numbers honestly: 749 Lean declarations, 14 axioms, 163 tracked sorries. Λ-uniqueness is Conjecture 1 — I don't claim theorems I haven't proved. That honesty is a deliberate competitive choice: at DoD-adjacent events where overclaiming gets punished, credibility is the moat.

Defense Unicorns published this as an unsolved problem at Warhacker 2026: "When a drone loses contact mid-mission — is the AI still operating within its authorized parameters, or has it gone off script? There's no independent system today that can monitor AI behavior in real time, catch the moment a line gets crossed, and back it up with a permanent, tamper-evident record." That is the Cannonico problem. SZL is the Cannonico answer.

SZL Holdings — five production organs, one signed mesh bundle:

Organ	Role	Live demo
a11oy	Signed-receipt substrate; receipts.in ≡ receipts.out audit-fiber
sentra	8-gate deny-by-default policy immune system; signed verdicts
amaru	Cited reasoning; refuses to fabricate; every answer receipted
killinchu	Counter-UAS edge organ; 13-axis Λ-gate; DSSE receipt per interdiction
rosie	Operator console; human-on-the-loop; cross-Space receipt verifier

All five ship as a single signed UDS bundle: uds deploy oci://ghcr.io/szl-holdings/szl-mesh:v0.4.0 --confirm

# Verify SLSA L2 provenance on any flagship (all five have it):
gh attestation verify oci://ghcr.io/szl-holdings/a11oy@sha256:1cfd28e03e6f1fb4b0827f2281f5016ebde8122d8c9ecb00d73145c77dd02cd7 \
  --repo szl-holdings/a11oy
# ✓ Verification succeeded

# Verify the signed bundle:
cosign verify oci://ghcr.io/szl-holdings/szl-mesh:v0.4.0 \
  --certificate-identity-regexp="^https://github.com/szl-holdings/" \
  --certificate-oidc-issuer="https://token.actions.githubusercontent.com"

# Full guide: https://github.com/szl-holdings/developers/blob/main/VERIFY.md

I do not claim "zero sorry," "fully verified," or "Λ proven." Every number above regenerates from lutar-lean@main. SLSA L3 is not claimed.

Concept DOI (always latest): 10.5281/zenodo.19944926

Languages: TypeScript · Python · Lean 4 · Bash
Runtime: Node.js 24 · pnpm · React · Vite · FastAPI
Data: PostgreSQL · Drizzle ORM · Redis · pgvector
Supply chain: Sigstore (SLSA L2) · Zenodo · CodeQL · Trivy · Gitleaks · OpenSSF Scorecard · SBOM
Observability: OpenTelemetry · 13-axis Λ-spans
Deployment: UDS Core / Zarf v0.77.0 · uds-cli v0.32.0 · Kubernetes / Istio Ambient

_{© 2026 Stephen P. Lutar Jr. · Code: Apache-2.0 · Research: CC BY 4.0 · Doctrine v11 LOCKED · Every count and DOI on this page verifiable against lutar-lean@main. Λ uniqueness is Conjecture 1. SLSA L2 verified (not L3).}

Signed-off-by: stephenlutar2-hash stephenlutar2@gmail.com