Spaces:
Running
Running
org-card: fix canonical numbers (4/12 Putnam, 626 decls, 189 sorries, 44 gates, Doctrine v7, 15 axioms), live scorecard badges, license split per Doctrine v7 §10
Browse files
README.md
CHANGED
|
@@ -11,44 +11,79 @@ short_description: Governed AI execution · verifiable receipts · formal proofs
|
|
| 11 |
|
| 12 |
<div align="center">
|
| 13 |
|
| 14 |
-
|
| 15 |
-
|
| 16 |
-
|
| 17 |
-
|
|
|
|
| 18 |
|
| 19 |
-
|
| 20 |
|
| 21 |
-
|
| 22 |
|
| 23 |
-
|
| 24 |
|
| 25 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 26 |
|
| 27 |
---
|
| 28 |
|
| 29 |
-
##
|
| 30 |
|
| 31 |
| | | |
|
| 32 |
|:-:|:-:|:-:|
|
| 33 |
-
|
|
| 34 |
| runtime gate | 17 tools | memory cortex |
|
| 35 |
-
|
|
| 36 |
| security gates | Lean 4 kernel | nervous / traces |
|
| 37 |
-
|
|
| 38 |
| operator console | runnable recipes | λ-gate loop |
|
| 39 |
|
| 40 |
---
|
| 41 |
|
| 42 |
-
##
|
| 43 |
|
| 44 |
-
|
|
| 45 |
-
|
|
| 46 |
-
|
|
|
|
|
|
|
|
| 47 |
|
| 48 |
---
|
| 49 |
|
| 50 |
-
##
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 51 |
|
| 52 |
-
|
| 53 |
|
| 54 |
-
|
|
|
|
|
|
|
|
|
|
|
|
| 11 |
|
| 12 |
<div align="center">
|
| 13 |
|
| 14 |
+
[](https://doi.org/10.5281/zenodo.20434276)
|
| 15 |
+
[](https://orcid.org/0009-0001-0110-4173)
|
| 16 |
+
[](https://securityscorecards.dev/viewer/?uri=github.com/szl-holdings/ouroboros)
|
| 17 |
+
[](https://securityscorecards.dev/viewer/?uri=github.com/szl-holdings/ouroboros-thesis)
|
| 18 |
+
[](https://securityscorecards.dev/viewer/?uri=github.com/szl-holdings/szl-uds-deployment)
|
| 19 |
|
| 20 |
+
</div>
|
| 21 |
|
| 22 |
+
---
|
| 23 |
|
| 24 |
+
## SZL Holdings λ
|
| 25 |
|
| 26 |
+
> Governance-mathematical AI execution with verifiable receipts and machine-checked formal proofs.
|
| 27 |
+
|
| 28 |
+
SZL Holdings builds governed AI infrastructure: a Lean 4 kernel for formal verification, COSE_Sign1 receipt chains for tamper-evident audit trails, and a policy gate system where every observable claim is backed by a checkable proof or a signed artifact. The operating doctrine is publicly versioned and machine-readable.
|
| 29 |
+
|
| 30 |
+
---
|
| 31 |
+
|
| 32 |
+
## Invariants
|
| 33 |
+
|
| 34 |
+
| Item | Value |
|
| 35 |
+
|---|---|
|
| 36 |
+
| Doctrine | v7 |
|
| 37 |
+
| Axioms | 15 (14 unique) |
|
| 38 |
+
| Lean 4 declarations | 626 |
|
| 39 |
+
| Sorries | 189 (138 baseline · 51 Putnam) |
|
| 40 |
+
| Anchor formula gates | 44 |
|
| 41 |
+
| Mathlib version | v4.13.0 |
|
| 42 |
+
| Putnam Lean-discharged | 4/12 GREEN (A1, A5, B4, B6) |
|
| 43 |
+
| Putnam structure coverage | 10/12 |
|
| 44 |
+
| SLSA | L1 (honest) |
|
| 45 |
+
| Spaces | 26 |
|
| 46 |
+
| Datasets | 29 |
|
| 47 |
+
| Models | 2 |
|
| 48 |
|
| 49 |
---
|
| 50 |
|
| 51 |
+
## The stack
|
| 52 |
|
| 53 |
| | | |
|
| 54 |
|:-:|:-:|:-:|
|
| 55 |
+
| ⚡ [a11oy](https://huggingface.co/spaces/SZLHOLDINGS/a11oy-receipts-playground) | ⛓ [MCP](https://huggingface.co/spaces/SZLHOLDINGS/mcp-receipts-server) | ◆ [amaru](https://huggingface.co/spaces/SZLHOLDINGS/amaru) |
|
| 56 |
| runtime gate | 17 tools | memory cortex |
|
| 57 |
+
| ⊕ [sentra](https://huggingface.co/spaces/SZLHOLDINGS/sentra-security-gates) | λ [lutar-lean](https://huggingface.co/spaces/SZLHOLDINGS/lutar-lean-browser) | ∮ [vsp-otel](https://huggingface.co/spaces/SZLHOLDINGS/vsp-otel-emitter) |
|
| 58 |
| security gates | Lean 4 kernel | nervous / traces |
|
| 59 |
+
| ∇ [rosie](https://huggingface.co/spaces/SZLHOLDINGS/rosie-operator-console) | ⊗ [cookbook](https://huggingface.co/spaces/SZLHOLDINGS/szl-cookbook-runner) | ∞ [ouroboros](https://huggingface.co/spaces/SZLHOLDINGS/ouroboros-lambda-gate) |
|
| 60 |
| operator console | runnable recipes | λ-gate loop |
|
| 61 |
|
| 62 |
---
|
| 63 |
|
| 64 |
+
## Citable releases
|
| 65 |
|
| 66 |
+
| Version | DOI |
|
| 67 |
+
|---|---|
|
| 68 |
+
| Ouroboros Thesis v18.0 | [10.5281/zenodo.20434276](https://doi.org/10.5281/zenodo.20434276) |
|
| 69 |
+
| Lean proof substrate (lutar-lean v18.0.0) | [10.5281/zenodo.20434308](https://doi.org/10.5281/zenodo.20434308) |
|
| 70 |
+
| Concept DOI (always-latest) | [10.5281/zenodo.19944926](https://doi.org/10.5281/zenodo.19944926) |
|
| 71 |
|
| 72 |
---
|
| 73 |
|
| 74 |
+
## License split
|
| 75 |
+
|
| 76 |
+
| Layer | License |
|
| 77 |
+
|---|---|
|
| 78 |
+
| Runtime | Apache-2.0 |
|
| 79 |
+
| Platform | BSL-1.1 |
|
| 80 |
+
| Research | CC-BY-4.0 |
|
| 81 |
+
|
| 82 |
+
---
|
| 83 |
|
| 84 |
+
## Verification
|
| 85 |
|
| 86 |
+
- [GitHub](https://github.com/szl-holdings) — source, CI, releases
|
| 87 |
+
- ORCID [0009-0001-0110-4173](https://orcid.org/0009-0001-0110-4173)
|
| 88 |
+
- Scorecard badges above are live and dynamic — they reflect the current OSSF Scorecard score for each repo
|
| 89 |
+
- Banner: [hero.svg](https://huggingface.co/spaces/SZLHOLDINGS/README/resolve/main/hero.svg) — v7 zero-text, geometric animations only
|