SZL Holdings — Formal Verification + Governance Receipts
Collection
Lean 4 theorems, DSSE receipts, OTel dataset, MCP server, and thesis. Agentic AI governance with machine-checked proofs. DOI 10.5281/zenodo.20434276 • 5 items • Updated
a11oy v19 Substrate — Governance Policy Model
-blue?style=flat-square){kind=icon}
Doctrine v11 LOCKED. No marketing. Every number resolves to a CI log, a Lean proof, or a Zenodo DOI.
Governance policy model card for a11oy v19 — the governed execution fabric organ. Policy weights are DSSE-signed at training time and verified against the Lean kernel at lutar-lean@c7c0ba17. 9 packages, 248 unit assertions.
The model encodes the 44-formula anchor gate set as hard policy constraints. No agentic action passes without clearing all 44 anchor formula gates. RAE-1 protocol (a11oy#122) defines the authorization handshake sequence.
Source: a11oy-source dataset. Live receipts: a11oy Space. DOI: 10.5281/zenodo.20431181.
State (live 2026-05-30)
| Metric | Value | Verify |
|---|---|---|
| Lean declarations | 749 | lutar-lean@c7c0ba17 |
| Lean axioms | 15 (14 unique) | A1–A18 honest gap |
| Lean sorries | 112 baseline + 51 Putnam = 163 total | lutar-lean@c7c0ba17 |
| Anchor formulas | 44 specified | a11oy#114 |
| Kernel green | Mathlib 4.13.0 d7317655 | PR #106 |
| HF Spaces | 13 | SZLHOLDINGS org |
| HF Datasets | 28 | SZLHOLDINGS org |
| Zenodo DOIs | 6 release + 1 concept alias | 10.5281/zenodo.20434276 |
| RAE-1 protocol | merged | a11oy#122 |
| Putnam honest | 10/12 | agi-forecast |
Cross-references
- Thesis: Ouroboros Thesis v18 · DOI 10.5281/zenodo.20434276
- Lean companion: lutar-lean · DOI 10.5281/zenodo.20424992
- Receipts: MCP server · szlholdings-hatun-mcp.hf.space
- Test results: SZLHOLDINGS/test-results
- Catalog: SZLHOLDINGS on HuggingFace
- Source: a11oy-v19-substrate on GitHub
Provenance
| Field | Value |
|---|---|
| Ecosystem stage | operational |
| Ecosystem stage matrix | SZLHOLDINGS org |
| MCP gateway | szlholdings-hatun-mcp.hf.space |
| Doctrine | v11 LOCKED (749/14/163 @ c7c0ba17) — no marketing language, every number resolves to a CI log or Zenodo DOI |
| Thesis DOI | 10.5281/zenodo.20434276 |
| Lean companion DOI | 10.5281/zenodo.20424992 |
| Author | Stephen Paul Lutar Jr. · ORCID 0009-0001-0110-4173 |
SZLHOLDINGS · 13 Spaces / 28 datasets / 3 models · Lean 749 decl / 14 unique axioms / 163 sorries (112 baseline + 51 Putnam) · 12 MCP tools · 6 release DOIs + 1 concept alias · HF org · Doctrine v11 LOCKED @ c7c0ba17
Inference Providers NEW
This model isn't deployed by any Inference Provider. 🙋 Ask for provider support