Hanzo Formal Proofs

Machine-checked and paper proofs for Hanzo AI Chain (= Lux A-Chain under Hanzo branding) and the Hanzo agent / inference settlement stack.

Inventory

File	Topic	Status
`hanzo-ai-chain-soundness.tex`	A-Chain (AIVM) attestation pipeline soundness	paper
`hanzo-adopts-liquidity-protocol.tex`	Hanzo formal adoption of the (2026-04-20)	paper
`lean/`	Lean 4 sources (shared with `luxfi/proofs/lean/`)	typecheck

Provenance

The Hanzo AI Chain is the Lux A-Chain (AIVM) deployed under the Hanzo brand. All low-level consensus, finality, and post-quantum security properties are inherited verbatim from luxfi/proofs:

quasar-cert-soundness.tex (LP-105 / Theorems 7.5-7.8)
lean/Consensus/Quasar.lean
lean/Crypto/{BLS,MLDSA,Corona}.lean
lean/Consensus/DAGEVM.lean (Block-STM serialisability)

This repo adds AI-specific lemmas:

Model-provenance commitment (every inference receipt commits to a model-hash).
Agent-identity binding via DID (did:lux:agent:*).
TEE attestation chain (Nitro Enclaves + AMD SEV-SNP, Hanzo attestation pre-compile per LP-127).
Inference-receipt settlement atomicity over the (post 2026-04-20 adoption).

Build

cd lean && lake build           # Lean 4 (shared with luxfi/proofs)
tectonic hanzo-ai-chain-soundness.tex
tectonic hanzo-adopts-liquidity-protocol.tex

Citations

Canonical references:

~/work/lux/lps/TAXONOMY.md (forbidden upstream names; A-Chain = AIVM)
~/work/lux/lps/LP-127-attestation.md
~/work/lux/lps/LP-130-ai.md
~/work/lux/lps/LP-134-lux-chain-topology.md
~/work/hanzo/papers/hanzo-ai-chain/hanzo-ai-chain.tex

Chronology

See CHRONOLOGY.md.

1.7 KiB Raw Permalink Blame History