Hugging Face's logo

SZLHOLDINGS
/
SZLHOLDINGS

Model card Files
xet
 Community
SZL Holdings λ — animated glyph

animated SVG — SMIL write-on loop · 3.5 s · parchment + terracotta · IBM Plex Mono · source: szl-visual-identity/animated/

SZL Holdings  λ

Formal verification · agentic AI substrate · governance receipts.

License Apache-2.0 CC-BY-4.0 Lean 4 SLSA L1 DOI ORCID GitHub

Lean 4 · Mathlib v4.13.0 · DSSE · SLSA Level 1 · OpenTelemetry · MCP · Opus 4.8 wrapper

Traction at a glance

Metric Value Verified
Thesis pages 206 doi:10.5281/zenodo.20434276
Theorems & corollaries 76 lutar-lean @ 23480eba
Lean-verified proofs 134 / 375 lake build · exit 0
a11oy alignment innovations 12 a11oy v19 · cbf10510
a11oy test suite 248 / 248 pass CI exit 0
UDS span records 100 uds-mesh @ 25a7e53e
DSSE attestation links 5 uds-spans-receipts dataset
Zenodo DOI records 7 concept → v18.0.0 software
GitHub repos 17 github.com/szl-holdings
HF artifacts 9+ all HTTP 200

Build receipts

OUROBOROS_RUN_ALL.py — all 25 modules PASS (rendered mockup from OUROBOROS_RUN_ALL.py @577b78c4 2026-05-28)

rendered mockup from OUROBOROS_RUN_ALL.py @577b78c4 · 25 modules · stdlib only · exit 0 · 2026-05-28

Thesis diagrams

Ouroboros Runtime Λ-Gate Impact Codex v11
Loop Impact Codex

10 figures from build_all.py · N = 10,000 · full gallery in thesis dataset

What we build

We build in three layers:

1 — Machine-checkable proof. The Ouroboros thesis v18 formalizes 76 theorems and corollaries across 206 pages in Lean 4 under Mathlib v4.13.0. Every invariant that governs agent behaviour has a proof object, not an assertion. Axiom A15 (SHA-256 collision resistance) is the one honest open problem; it cites NIST FIPS 180-4 and is not hidden.

2 — Runtime substrate. The a11oy v19 substrate wraps any Opus 4.8-class base model with 12 alignment innovations drawn from Constitutional AI (Bai et al. 2022), Sleeper Agents (Hubinger et al. 2024), Alignment Faking (Greenblatt et al. 2024), and Anthropic's RSP. It distributes no weights; it is a specification and test harness. 248 / 248 tests pass.

3 — Governance receipts. The UDS observability mesh emits OpenTelemetry spans wrapped in DSSE envelopes and attested at SLSA Level 1. The MCP receipts server exposes those receipts over four MCP tools, wirable into any MCP-compatible host.

Why governance receipts matter

Most AI safety claims are stated in natural language. We make the same claims in formal logic, run them through a proof checker (Lean 4 / Mathlib), attach signed attestation envelopes (DSSE), and serve them over a standard protocol (MCP). The result: every runtime safety property is checkable, not just readable.

This is not a product claim. It is a research posture: proof first, assertion second, no claim without evidence.

Artifacts

Artifact What it does License
📄 thesis-v18-formal-verification Read 206 pp of machine-checkable AI invariant theory CC-BY-4.0
🤖 a11oy-v19-substrate Run the 12-innovation alignment substrate on any Opus 4.8 base Apache-2.0
📡 uds-spans-receipts Inspect 100 OTel spans and 50 DSSE governance receipts CC-BY-4.0
🛠️ mcp-receipts-server Wire governance receipt lookup into Claude Desktop in 60 s Apache-2.0
📐 lutar-lean-browser Browse 375 theorems and inspect 134 lake-verified proofs live Apache-2.0
🎨 szl-visual-identity Fetch the canonical avatar, banner, and architecture diagrams CC-BY-4.0

What it looks like

MCP Receipts Server Lutar Lean Browser
MCP Governance Receipts Server — 5-tab Gradio overlay with JSON response (rendered mockup from mcp_receipts_server/app_overlay.py @577b78c4 2026-05-28) Lutar Lean Browser — chapter sidebar + theorem detail + View Source tab (rendered mockup from lutar_lean_space/app.py @23480eba 2026-05-28)
rendered mockup · mcp_receipts_server/app_overlay.py @577b78c4 rendered mockup · lutar_lean_space/app.py @23480eba
SZL Showcase a11oy Playground
SZL Showcase — 5-tab mega tour (rendered mockup from szl-showcase/app.py @577b78c4 2026-05-28) a11oy Receipts Playground — prompt input + DSSE receipt output (rendered mockup from a11oy-receipts-playground/app.py @cbf10510 2026-05-28)
rendered mockup · szl-showcase/app.py @577b78c4 rendered mockup · a11oy-receipts-playground/app.py @cbf10510

HF Organization

All anchor artifacts are grouped in one curated collection: SZL Holdings — Formal Verification + Governance Receipts

Companion GitHub organization: github.com/szl-holdings — 17 repos, DCO live, SBOM 13 / 18 complete, SLSA 8 / 8 release provenance attached.

Pattern credit: "HF Organization" section structure adapted from Mistral AI HF org.

Use-case deployment table

If you want to… Start here
Verify an AI safety invariant formally thesis-v18-formal-verification — theorem index, Table 1
Run the alignment substrate on your own agent a11oy-v19-substrate — Quick Start, pip install szl-a11oy
Inspect signed governance receipts uds-spans-receipts — Quick Start, datasets.load_dataset(...)
Add a receipt MCP tool to Claude Desktop mcp-receipts-server — 60-second wire-in
Browse all formalized theorems interactively lutar-lean-browser — live at the Space URL
Use official SZL visual assets szl-visual-identity — asset inventory table
Reproduce any result end-to-end github.com/szl-holdings/uds-mesh — make reproduce

Pattern credit: use-case decision table adapted from NVIDIA HF org.

Verification receipt 

org         SZLHOLDINGS
plan        team
role        admin (betterwithage)
artifacts   2 models · 4 datasets · 3 spaces — all HTTP 200
thesis      v18.0 · 206 pp · 76 theorems · 0 errors
lean        lutar-lean @ 23480eba · Mathlib v4.13.0
uds         uds-mesh @ uds-v0.2.0 · sha 25a7e53e
substrate   32 / 32 modules green · exit 0
dois        7 / 7 — all 200 — see register below
retrieved   2026-05-28

Supply-chain verify:

# Verify thesis DOI resolves
curl -sI https://doi.org/10.5281/zenodo.20434276 | grep -i location

# Verify software DOI resolves
curl -sI https://doi.org/10.5281/zenodo.20434308 | grep -i location

# Verify a11oy commit
curl -sI https://api.github.com/repos/szl-holdings/a11oy/commits/cbf10510 | grep -i x-ratelimit-remaining

# Verify UDS commit
curl -sI https://api.github.com/repos/szl-holdings/uds-mesh/commits/25a7e53e | grep -i x-ratelimit-remaining

DOI register 

concept        10.5281/zenodo.19944926   https://doi.org/10.5281/zenodo.19944926
v14            10.5281/zenodo.20424992   https://doi.org/10.5281/zenodo.20424992
v15            10.5281/zenodo.20424995   https://doi.org/10.5281/zenodo.20424995
v16            10.5281/zenodo.20424996   https://doi.org/10.5281/zenodo.20424996
v17            10.5281/zenodo.20431181   https://doi.org/10.5281/zenodo.20431181
thesis v18     10.5281/zenodo.20434276   https://doi.org/10.5281/zenodo.20434276
software       10.5281/zenodo.20434308   https://doi.org/10.5281/zenodo.20434308

Honest accounting — open problems

Problem Status Notes
Axiom A15 (SHA-256 collision resistance) Open — cited References NIST FIPS 180-4; no known collision
Lean proof skeleton count 241 of 375 skeletal Lake build passes on 134; full closure is ongoing
SLSA Level 3 build-chain Level 1 attained Level 3 requires hermetic build infra not yet deployed
Multi-agent invariant transfer Theoretical only Chapter 9 formalizes; runtime multi-agent harness not yet shipped
External adversarial red-team Not yet conducted Planned for v20 milestone

Pattern credit: honest limitations format adapted from Anthropic HF org and Mistral AI HF org.

Governance posture

  • All artifacts carry SPDX license headers.
  • Dataset artifacts carry Croissant metadata where applicable.
  • Model artifacts include SLSA Level 1 provenance attestations.
  • DCO sign-off is enforced on all GitHub commits.
  • Responsible AI statement: szlholdings.com/responsible-ai (forthcoming — link will resolve at v20 milestone).
  • No training data from third-party copyrighted works is included in any SZL dataset.

Pattern credit: governance posture section adapted from Google HF org responsible AI links pattern.

Team

Person Role ORCID
Stephen P. Lutar Founder · lead researcher · principal engineer 0009-0001-0110-4173

Contact: stephen@szlholdings.com

Cite this work

Thesis (v18):

@misc{lutar2026ouroboros,
  author       = {Lutar, Stephen P.},
  title        = {Ouroboros: Formal Verification of Agentic AI Invariants — Thesis v18},
  year         = {2026},
  publisher    = {Zenodo},
  doi          = {10.5281/zenodo.20434276},
  url          = {https://doi.org/10.5281/zenodo.20434276},
  note         = {Lean 4 · Mathlib v4.13.0 · 76 theorems · 206 pp}
}

Software (a11oy v19 substrate):

@software{lutar2026a11oy,
  author       = {Lutar, Stephen P.},
  title        = {SZL Holdings Software — a11oy v19 Substrate and UDS Mesh},
  year         = {2026},
  publisher    = {Zenodo},
  doi          = {10.5281/zenodo.20434308},
  url          = {https://doi.org/10.5281/zenodo.20434308},
  note         = {Apache-2.0 · commit cbf10510 · 248/248 tests pass}
}

Pattern credit: dual BibTeX block adapted from NVIDIA HF model cards and Meta-Llama HF model cards.

License posture

Surface License
Model & Space wrappers Apache-2.0
Datasets (thesis, UDS, visual identity) CC-BY-4.0
UDS internal components (a11oy/amaru/rosie/sentra) Proprietary — public surface via Apache-2.0 wrappers only

Every artifact ships with a verifiable LICENSE file, a CITATION.cff entry, and a Zenodo DOI where applicable.

Curated by betterwithage for SZL Holdings · Aesthetic: True Anomaly precision · Anthropic research minimalism · New Relic data density · Doctrine v6 · Series-A full graft 2026-05-28


λ   ·   proof   ·   runtime   ·   receipt

Downloads last month

-

Downloads are not tracked for this model. How to track
Inference Providers NEW
This model isn't deployed by any Inference Provider. 🙋 Ask for provider support

Papers for SZLHOLDINGS/SZLHOLDINGS