mirror of https://github.com/zooai/proofs.git synced 2026-10-30 14:49:47 +00:00

Files

T

zeekay c86eec94cb merge: absorb /Users/z/work/zoo/formal into proofs (de-duplicate)

Local zoo/formal was a stale parallel checkout that pointed at
zoo-labs/formal (non-existent); the canonical remote is
zooai/proofs. This commit absorbs the unique formal-verification
work from the old checkout into proofs:

- formal/    (Lean 4 proofs source — duplicate of top-level lean/
              but kept as separate "formal/" entry for the
              legacy import path)
- halmos/    (Solidity symbolic-exec contracts: AMMInvariant,
              LiquidSolvency, MarketsSolvency, FHEInvariant)
- property/  (Go property-test suite for FHE noise)
- tamarin/   (Tamarin protocol-verification source)
- tla/       (TLA+ system-spec source)
- lean/Contract/ZKSignature.lean  (unique, not in proofs/lean)
- lean/Crypto/ZKSignature.lean    (unique, not in proofs/lean)
- FORMAL_VERIFICATION.md (preserved from the old README)
- LLM-formal.md          (preserved from the old LLM.md)

The duplicate folder /Users/z/work/zoo/formal is now deleted on
disk. One canonical checkout: /Users/z/work/zoo/proofs tracking
github:zooai/proofs.

2026-05-12 21:13:00 -07:00

2.2 KiB

Raw Permalink Blame History

Zoo Formal Verification

21 machine-checked proofs for Zoo Network's critical systems.

Proof Inventory

Lean 4 (14 proofs)

AI Systems:

Proof	Property
`AI/DSO.lean`	Decentralized Semantic Optimization convergence and safety
`AI/Embedding.lean`	Embedding space metric properties
`AI/ExperienceLedger.lean`	Experience ledger Byzantine fault tolerance
`AI/Gym.lean`	Training platform correctness
`AI/Personalization.lean`	Privacy guarantees for personalization

Smart Contracts:

Proof	Property
`Contract/AMM.lean`	Automated Market Maker solvency invariants
`Contract/Bridge.lean`	Cross-chain bridge safety
`Contract/Staking.lean`	Staking mechanism security
`Contract/Token.lean`	Token contract properties

Governance:

Proof	Property
`Governance/AgentNFT.lean`	Agent ownership and transfer
`Governance/Compensation.lean`	Reward distribution fairness
`Governance/Contribution.lean`	Contribution tracking integrity
`Governance/Treasury.lean`	Treasury management invariants
`Governance/ZIP.lean`	Proposal mechanism correctness

TLA+ (2 specs)

Spec	Property
`tla/Wave.tla`	Protocol wave behavior
`tla/MC_Wave.tla`	Model checker configuration

Halmos (4 symbolic tests)

Test	Property
`halmos/AMMInvariant.t.sol`	AMM solvency under all inputs
`halmos/LiquidSolvency.t.sol`	Liquidity protocol solvency
`halmos/MarketsSolvency.t.sol`	Market solvency properties
`halmos/test/FHEInvariant.t.sol`	FHE noise budget invariants

Tamarin (1 protocol proof)

Proof	Property
`tamarin/RNSHybridHandshake.spthy`	RNS hybrid handshake security

Property-Based Testing (Go)

Test	Property
`property/fhe_noise_test.go`	FHE noise growth bounds

Build

# Lean 4
cd lean && lake build

# Halmos
halmos --contract AMMInvariant

# TLA+
tlc MC_Wave.tla

# Tamarin
tamarin-prover RNSHybridHandshake.spthy

Authors

Antje Worring & Zach Kelling — Zoo Labs Foundation

2.2 KiB Raw Permalink Blame History