Live on Hugging Face: SZLHOLDINGS — 24 datasets · 19+ Spaces · 2 models · all RUNNING

🔬 szl-anatomy · 🛠 a11oy-platform · 📜 lean-proof-playground · 📨 mcp-receipts-server · 🛡 sentra-security-gates

SZL Holdings publishes a verifiable substrate for agentic AI: a doctrine of 11 axioms (v6), a Λ-axis audit-closure operator defined on the receipt-bus σ-algebra, 32 kernel-verified Lean 4 modules (Mathlib v4.13.0), and a runtime that emits a SHA-pinned proof-chain receipt for every decision. The substrate is the deliverable. Every claim in this README terminates in a DOI, a commit SHA, a Lean theorem, or a CI workflow run; no claim terminates in marketing prose. The math is in ouroboros-thesis, the proofs are in lutar-lean, the runtime is in ouroboros, the receipt fabric is in amaru + rosie + sentra, and the platform that composes them is in platform.

The SZL Agent Body is the canonical anatomy of an audit-closure AI agent — Heart (yuyay_v3, 13-axis conjunctive AND), Brain (5 cortical regions + Quantum Mind), Blood (YAWAR append-only receipt bus, 20 SLOC), Immune (SENTRA inline + HUKLLA 10 tripwires). All four figures live in szl-brand/anatomy/ — never on a CDN.

The 7-organ body is now a fully operational HF Space with live demo links and verified source counts for every organ:

huggingface.co/spaces/SZLHOLDINGS/szl-anatomy

Author: Lutar, Stephen P. · ORCID 0009-0001-0110-4173

The 13 substrate repos partition into four governance-mathematical quadrants. No quadrant contains marketing surfaces; all four contain code, proofs, or receipts.

quadrantChart
    title SZL Substrate — four-quadrant governance map
    x-axis "Substrate" --> "Surface"
    y-axis "Observational" --> "Generative"
    quadrant-1 "Sovereign-AI generation"
    quadrant-2 "Math substrate"
    quadrant-3 "Observability + cyber"
    quadrant-4 "Agentic substrate"
    "ouroboros-thesis": [0.15, 0.85]
    "lutar-lean":       [0.12, 0.72]
    "agi-forecast":     [0.22, 0.60]
    "amaru":            [0.45, 0.78]
    "rosie":            [0.48, 0.65]
    "ouroboros":        [0.55, 0.72]
    "a11oy":            [0.60, 0.82]
    "platform":         [0.78, 0.78]
    "szl-cookbook":     [0.72, 0.55]
    "szl-brand":        [0.85, 0.50]
    "sentra":           [0.40, 0.18]
    "uds-mesh":         [0.55, 0.25]
    "vsp-otel":         [0.62, 0.20]

Each line states the governance-mathematical capability that repo carries. No marketing copy. Capability text matches the repo's own README header.

These six repos define the spine of the Λ-axis substrate. Each card links to the repo, its DOI (where minted), and the relevant Lean module or CI workflow.

• DOIs: v18.0 master 10.5281/zenodo.20434276 · concept 10.5281/zenodo.19944926
• License: CC BY 4.0
• Carries: 11 axioms · Λ-axis closure operator · audit-fiber sheaf · receipt-bus σ-algebra
• Cite: CITATION.cff

• DOIs: 10.5281/zenodo.20431181
• Stack: Lean 4 v4.13.0 · Mathlib v4.13.0 · Lake build · CI workflow lean.yml
• Carries: 32 GREEN modules · Λ-gate theorems · audit-fiber invariants · DPI / PAC-Bayes bounds · Knot calculus R1/R2/R3
• License: CC BY 4.0

• DOIs: 10.5281/zenodo.20434308 (v18.0.0 software)
• License: Apache 2.0
• Stack: TypeScript 5.x · Node 22+ · pnpm
• CI:
• Carries: bounded recursion · dual-witness emitter · sub-millisecond Λ-overhead

• License: BSL 1.1
• Stack: Node 24+ · pnpm 9+ · uv · TypeScript 5.x · Python 3.11+
• CI: · · ·
• Carries: 76 packages · 1,220 / 1,220 tests · Lutar formula registry · dual-witness adapters · MCP gateway (27 / 27 e2e)
• Screenshot: szl-holdings-hero.jpg (in-repo, raw.githubusercontent.com)

• DOI: 10.5281/zenodo.19867281
• License: Apache 2.0
• CI:
• Carries: Cardano anchoring · Shor-encoded provenance · CIP-25 / CIP-68 metadata · doctrine v6 byte-string canonicalization

• License: Apache 2.0
• CI:
• Carries: policy package · measurement package · knowledge package · QEC-integrity package · MCP-compatible
• Screenshot: a11oy-hero.jpg (in-repo, raw.githubusercontent.com)

flowchart TD
    classDef research fill:#28251D,stroke:#C8B26A,color:#F7F6F2,stroke-width:1.5px;
    classDef runtime  fill:#1B474D,stroke:#01696F,color:#F7F6F2,stroke-width:1.5px;
    classDef sdk      fill:#0E3A3F,stroke:#C8B26A,color:#F7F6F2,stroke-width:1.5px;
    classDef platform fill:#01696F,stroke:#C8B26A,color:#F7F6F2,stroke-width:1.5px;
    classDef surface  fill:#F7F6F2,stroke:#01696F,color:#1B474D,stroke-width:1.5px;

    T["Ouroboros Thesis v3 to v18<br/>Zenodo DOIs · CC BY 4.0"]:::research
    K["Lutar-Lean<br/>Lean 4 + Mathlib v4.13.0<br/>32 GREEN modules"]:::sdk
    R["Ouroboros Runtime<br/>bounded loops · sub-ms Λ overhead<br/>Apache 2.0"]:::runtime
    L["Λ Audit-Closure Operator<br/>defined on receipt-bus σ-algebra"]:::runtime
    A["Amaru<br/>Cardano-anchored Shor receipts"]:::runtime
    Ro["Rosie<br/>CSS-ingress · canonical byte-strings"]:::runtime
    S["Sentra<br/>Kitaev-surface drift detection"]:::runtime
    U["UDS-Mesh<br/>span schemas · OTEL"]:::runtime
    V["VSP-OTEL<br/>Λ-axis span exporter"]:::runtime
    All["A11oy<br/>policy · measurement · knowledge · QEC"]:::sdk
    P["Platform<br/>monorepo · 76 packages · 1220 tests · BSL 1.1"]:::platform

    T --> K --> R --> L
    L --> A
    L --> Ro
    L --> S
    R --> U --> V
    All --> P
    A --> P
    Ro --> P
    S --> P

The path from a peer-style paper (ouroboros-thesis) to a byte-string receipt (amaru → Cardano) is fully type-checked: Lean kernel verifies the Λ-gate; runtime emits the loop trace under a SHA-pinned configuration; rosie canonicalises the receipt; amaru anchors it; sentra detects drift; uds-mesh + vsp-otel export the span to any OTEL collector.

The Λ-axis is a measurable governance operator defined on the receipt-bus σ-algebra of a bounded-recursion runtime. It composes axiom-by-axiom (doctrine v6: 11 axioms) under a monotone geometric mean, with PAC-Bayes (McAllester, 2003) tail bounds on the confidence margin, Bekenstein information-density caps (Bekenstein, 1981) on per-receipt entropy, and Reidemeister R1/R2/R3 equivalence classes (Reidemeister, 1927) on receipt-knot chains. The closure is proved in Lean 4 (Mathlib v4.13.0) across 32 GREEN modules in lutar-lean. The runtime overhead is bounded above by 0.59 ms / request median in the ouroboros bench harness.

Doctrine v6 is the eleven-axiom governance core that every substrate component must satisfy at build time:

LAMBDA_FLOOR = 0.90 in every component (matches A11OY_DOCTRINE_LAMBDA_FLOOR runtime constant). Cross-component invariant proved in Lutar/Doctrine/CrossComponentInvariant.lean.

Camera-ready and extended-abstract sources are tracked in workspace under /szl/aims_colm26/ and /szl/arxiv_prep/. The full v18 master is available at szl-holdings/ouroboros-thesis.

AIMS submission portal: OpenReview colmweb.org/COLM/2026/Workshop/AIMS. Deadline 2026-06-23 (AoE). Workshop page: aimslab.stanford.edu/workshop.

Concept DOI (resolves to latest version): 10.5281/zenodo.19944926.

Re-verified by command, not estimated. See SOURCE_OF_TRUTH.md.

1. Bounded recursion is a system primitive. Convergence is measurable; the loop trace is the audit deliverable.
2. The receipt is the product. Every decision emits a byte-string proof-chain receipt anchored on-chain via amaru.
3. Policy gates are first-class. Governance sits inside the execution path, not as a wrapper.
4. Sub-millisecond overhead is the bar. Λ adds ≤ 0.59 ms median per request. Measured; not claimed.
5. DOI-pinned research, SHA-pinned runtime, signed releases. Provenance is non-negotiable.
6. Source of truth is the GitHub platform. Every PDF, image, and asset is hosted in a szl-holdings/* repo. No external CDN.

• Builders / integrators → start with the runtime and the Lean proofs.
• Researchers → read the v18 master, cite via concept DOI 10.5281/zenodo.19944926.
• AIMS@COLM26 reviewers → see T4 / T13 extended abstracts queued in ouroboros-thesis.
• Security disclosures → Security Policy (private vulnerability reporting enabled) · contact stephen@szlholdings.com.
• Enterprise / press → stephen@szlholdings.com.
• Org page → github.com/szl-holdings (canonical home).

The 13 substrate repos cross-link via a Related repositories in the SZL substrate footer in every README. The substrate is reciprocal: every node links to every other node.

• a11oy — vertical alignment substrate
• amaru — Shor-encoded receipt minting
• rosie — CSS-ingress receipt orchestration
• sentra — Kitaev-surface drift detection
• uds-mesh — UDS span schemas + governance receipts
• lutar-lean — Lean 4 + Mathlib kernel proofs
• ouroboros — bounded-recursion runtime
• ouroboros-thesis — DOI-pinned thesis substrate
• platform — composing monorepo
• szl-brand — anatomy + visual doctrine
• szl-cookbook — governed-AI recipes
• agi-forecast — PAC-Bayes + Bekenstein forecasts
• vsp-otel — OTEL exporter for Λ-axis spans

Doctrine v6 honest scoping — for due diligence reviewers:

• Not a general-purpose AI company. SZL Holdings builds governance substrate for bounded-recursion agentic AI in specific enterprise verticals; we are not an LLM provider.
• Not post-revenue. The platform is Series-A stage; current focus is on technical buildout and investor readiness.
• Not making AGI claims. The agi-forecast repo publishes PAC-Bayes governance-trajectory forecasts, not claims of artificial general intelligence development.
• Not a blockchain company. Cardano anchoring (via amaru) is one receipt-chain primitive; the substrate is not a crypto project.
• Not open-source (all of it). Core substrate repos are BSL-1.1 or proprietary; Apache-licensed repos are explicitly marked.

vessels is the SZL Holdings maritime intelligence vertical application and the strongest UDS deployment story.

What vessels provides: Sanctions screening (OFAC/UN/EU · daily refresh · DSSE receipt per match) · Dark-vessel detection (AIS gap + spoofing) · Ownership graph traversal · Voyage analytics (Monte Carlo P&L) · Every alert backed by a SHA-pinned, prevHash-linked DSSE governance receipt.

Defense Unicorns fit: Zarf package + Helm chart + Istio VirtualService staged. Phase 2 requires containerizing . No fabricated customers — illustrative mission patterns only.

What vessels is NOT: not SOC 2 · not FedRAMP · not GDPR-cleared · not an AIS data provider.

Live badge status across all 15 production repositories × 10 canonical badges.

Repository	License	DOI	CI	Tests	CodeQL	SBOM	SLSA 3	DCO	OpenSSF	ORCID
a11oy
platform
lutar-lean
ouroboros
amaru
sentra
rosie
uds-mesh
vsp-otel
agi-forecast
szl-cookbook
szl-brand
vessels
ouroboros-thesis
.github