SZL HoldingsGoverned AI, proven in Lean.

What is SZL? ​

SZL Holdings builds governed-AI infrastructure: an anatomy of composable organs that turns a model from a thing that evaluates into an agent that acts under proof. The core claim is narrow and falsifiable — an action is "agentic" only if it is Λ-bounded, Yuyay-gated, HUKLLA-safe, and Khipu-receipted — and it is stated as a single Lean-checkable operator, P(x,t), defined in Doctrine v12 (PURIQ).

Everything ships under the Zero-Bandaid Law: every formula is Lean-stateable (open goals are sorry-tagged, never hidden), every claim is verifiable on disk, and every act emits a receipt. We use no mystical language anywhere — every name below is either a cited Quechua common noun or a math primitive carried from the formal corpus.

The Lean corpus that backs these claims is, at the Doctrine v11 lock, 749 declarations · 14 unique axioms · 163 tracked sorries, with a 13-axis yuyay_v3 heart whose replay hash is bacf54434f1a3bf2d758b27a62d5fd580ca4c8d3b180693573eeebcaea631fc5 (see Doctrine v11 + v12 for the locked register and Evidence for reproduction commands).

The flagships ​

Two flagships ship today — a11oy and killinchu — alongside three frontier/roadmap components surfaced under honest role names. Each is cross-referenced to the Ouroboros Thesis (DOI 10.5281/zenodo.20434276) and the Lean kernel lutar-lean.

The internal codenames amaru, rosie, and sentra are retired; the honest, user-facing names are Provenance Anchor, Operator, and Policy. Quechua glosses follow the standard lexica at kaikki.org Quechua; killinchu = "kestrel". a11oy is an SZL coinage (the alloy metaphor), not a Quechua word — labelled honestly as such.

Core & proof ​

Beyond the flagships, two repositories carry the load-bearing evidence:

• lutar-lean / lean-kernel — the machine-checked Lean proof corpus (749 declarations / 14 axioms / 163 sorries at c7c0ba17). See Proof.
• szl-lake — the public attestation lake: DSSE receipts, doctrine snapshots, Khipu chains, SBOMs. See Data Lake.

Start here ​

• Quickstart — five minutes to a first call against the shipping flagships.
• Architecture — the 7-organ anatomy and the master action-selection operator.
• Anatomy + Organs — the twelve organs, each with its Quechua etymology, function, formula, and Lean stub.
• 3D Showcases — interactive Anatomy-3D and Operator receipt-DAG visualizers.
• Proof — Lean kernel, data lake, and Zenodo DOIs.
• Changelog — aggregated v1.0.0 release notes (Keep a Changelog).
• UDS — Deploy & Hand-off — sign-verify-deploy a flagship as a UDS payload.
• Compliance & Security — honest posture: SLSA L1, cosign PENDING, certification roadmap.

Citation ​

If you build on SZL, please cite the archived release:

@software{szl_holdings_2026,
  author    = {Lutar, Stephen P.},
  title     = {SZL Holdings: Sovereign Governed AI --- a formally-verified governance substrate for agentic systems},
  year      = {2026},
  publisher = {Zenodo},
  version   = {Doctrine v11 LOCKED},
  doi       = {10.5281/zenodo.20434276},
  url       = {https://github.com/szl-holdings},
  note      = {749 declarations / 14 axioms / 163 sorries, kernel c7c0ba17}
}

Built with / learned from ​

Our documentation and publication conventions were learned from open-source leaders — we adapted their patterns, not their words. Inspired by patterns from Polymathic AI (the_well, walrus), Anthropic, OpenAI (whisper), Stripe (docs craft), Google DeepMind (alphafold3), Meta FAIR (segment-anything), EleutherAI (lm-evaluation-harness), and Hugging Face (transformers). We are a precision substrate, not a vibes company.