README.md

---
title: amaru Platform — Memory Attestation
emoji: 🔬
colorFrom: indigo
colorTo: gray
sdk: static
pinned: false
license: apache-2.0
short_description: "Static platform doc: amaru memory organ"
tags:
  - formal-verification
  - lean4
  - mathlib
  - dsse
  - governance
  - agentic-ai
  - arxiv:2401.05566
  - arxiv:2407.11214
  - series-a
  - anthropic
  - doctrine-v6
  - rae-1
  - amaru
  - memory
  - attestation
  - platform
ecosystem-stage: release-payload
---

# amaru Platform — Memory Attestation

[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.20434276.svg)](https://doi.org/10.5281/zenodo.20434276)
[![Lean Kernel Green](https://img.shields.io/badge/Lean_4.13-kernel--green-22c55e?style=flat-square)](https://github.com/szl-holdings/lutar-lean/pull/106)
[![Sorries](https://img.shields.io/badge/sorries-5-blue?style=flat-square)](https://github.com/szl-holdings/lutar-lean/pull/109)
[![SLSA L1](https://img.shields.io/badge/SLSA-L1_SBOM+DCO-blue?style=flat-square)](https://slsa.dev)
[![DSSE](https://img.shields.io/badge/DSSE-PAE_v1-22c55e?style=flat-square)](https://slsa.dev/dsse)
[![RAE-1](https://img.shields.io/badge/RAE--1-v1.0-D97757?style=flat-square)](https://huggingface.co/datasets/SZLHOLDINGS/test-results)
[![MCP](https://img.shields.io/badge/MCP-server_live-ff6b35?style=flat-square)](https://huggingface.co/spaces/SZLHOLDINGS/mcp-receipts-server)
[![License](https://img.shields.io/badge/License-Apache_2.0-blue?style=flat-square)](https://www.apache.org/licenses/LICENSE-2.0)

> **Doctrine v6.** No marketing. Every number resolves to a CI log, a Lean proof, or a Zenodo DOI.

Static documentation site for amaru — the memory-attestation organ of the SZL substrate. Covers hash-chain architecture, DSSE receipt format, context persistence guarantees, and integration with the a11oy execution fabric.

Memory operations are gated by the RAE-1 protocol. Each session context is attested at write time and verifiable via the [amaru-memory-attestation space](https://huggingface.co/spaces/SZLHOLDINGS/amaru-memory-attestation).

## State (live 2026-05-30)

| Metric | Value | Verify |
|---|---|---|
| Lean declarations | 217 | [lutar-lean@7ef33a6](https://github.com/szl-holdings/lutar-lean/commit/7ef33a6) |
| Lean axioms | 12 | A1–A18 honest gap |
| Lean sorries | 5 (was 7) | [PR #109 discharged P6+P7](https://github.com/szl-holdings/lutar-lean/pull/109) |
| Anchor formulas | 35/35 as gates | [a11oy#114](https://github.com/szl-holdings/a11oy/pull/114) |
| Kernel green | Mathlib 4.13.0 d7317655 | [PR #106](https://github.com/szl-holdings/lutar-lean/pull/106) |
| HF Spaces | 24 | [SZLHOLDINGS org](https://huggingface.co/SZLHOLDINGS) |
| HF Datasets | 29 | [SZLHOLDINGS org](https://huggingface.co/SZLHOLDINGS) |
| Zenodo DOIs | 7 | [10.5281/zenodo.20434276](https://doi.org/10.5281/zenodo.20434276) |
| RAE-1 protocol | merged | [a11oy#122](https://github.com/szl-holdings/a11oy/pull/122) |
| Putnam honest | 10/12 | [agi-forecast](https://github.com/szl-holdings/agi-forecast) |

## Cross-references

- **Thesis**: [Ouroboros Thesis v18](https://doi.org/10.5281/zenodo.20434276) · DOI 10.5281/zenodo.20434276
- **Lean companion**: [lutar-lean](https://doi.org/10.5281/zenodo.20424992) · DOI 10.5281/zenodo.20424992
- **Receipts**: [MCP server](https://huggingface.co/spaces/SZLHOLDINGS/mcp-receipts-server) · szlholdings-mcp-receipts-server.hf.space
- **Test results**: [SZLHOLDINGS/test-results](https://huggingface.co/datasets/SZLHOLDINGS/test-results)
- **Catalog**: [SZLHOLDINGS on HuggingFace](https://huggingface.co/SZLHOLDINGS)
- **Source**: [amaru-platform on GitHub](https://github.com/szl-holdings/szl-holdings)


## Provenance

| Field | Value |
|---|---|
| Ecosystem stage | `release-payload` |
| Ecosystem stage matrix | [SZLHOLDINGS/szl-anatomy → Stage Matrix](https://huggingface.co/spaces/SZLHOLDINGS/szl-anatomy) |
| MCP gateway | [szlholdings-mcp-receipts-server.hf.space](https://szlholdings-mcp-receipts-server.hf.space) |
| Doctrine | v6 — no marketing language, every number resolves to a CI log or Zenodo DOI |
| Thesis DOI | [10.5281/zenodo.20434276](https://doi.org/10.5281/zenodo.20434276) |
| Lean companion DOI | [10.5281/zenodo.20424992](https://doi.org/10.5281/zenodo.20424992) |
| Author | Stephen Paul Lutar Jr. · [ORCID 0009-0001-0110-4173](https://orcid.org/0009-0001-0110-4173) |
---

*SZLHOLDINGS · 24 Spaces / 29 datasets / 2 models · Lean 217 decl / 12 axioms / 5 sorries · 35/35 gates · 7 Zenodo DOIs · [HF org](https://huggingface.co/SZLHOLDINGS) · [MCP gateway](https://szlholdings-mcp-receipts-server.hf.space) · [Stage matrix](https://huggingface.co/spaces/SZLHOLDINGS/szl-anatomy) · Doctrine v6*