mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekay
c86eec94cb
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.
114 lines
1.9 KiB
Lean4
114 lines
1.9 KiB
Lean4
import Lake
|
|
open Lake DSL
|
|
|
|
package luxFormal where
|
|
leanOptions := #[
|
|
⟨`autoImplicit, false⟩
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Consensus where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Consensus.Safety,
|
|
`Consensus.Liveness,
|
|
`Consensus.BFT,
|
|
`Consensus.Quasar,
|
|
`Consensus.Finality,
|
|
`Consensus.Validator,
|
|
`Consensus.ThresholdProof,
|
|
`Consensus.PreferenceStability
|
|
]
|
|
|
|
lean_lib Protocol where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Protocol.Wave,
|
|
`Protocol.Flare,
|
|
`Protocol.Ray,
|
|
`Protocol.Field,
|
|
`Protocol.Quasar,
|
|
`Protocol.Nova,
|
|
`Protocol.Nebula,
|
|
`Protocol.Photon,
|
|
`Protocol.Prism,
|
|
`Protocol.Handshake
|
|
]
|
|
|
|
lean_lib Crypto where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Crypto.BLS,
|
|
`Crypto.FROST,
|
|
`Crypto.Corona,
|
|
`Crypto.MLDSA,
|
|
`Crypto.Hybrid,
|
|
`Crypto.SLHDSA,
|
|
`Crypto.MLKEM,
|
|
`Crypto.FHE.TFHE,
|
|
`Crypto.FHE.CKKS,
|
|
`Crypto.Threshold.CGGMP21,
|
|
`Crypto.Threshold.LSS,
|
|
`Crypto.Threshold.Composition,
|
|
`Crypto.VerkleTree
|
|
]
|
|
|
|
lean_lib Warp where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Warp.Delivery,
|
|
`Warp.Ordering,
|
|
`Warp.Security
|
|
]
|
|
|
|
lean_lib Trust where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Trust.Authority,
|
|
`Trust.Vouch,
|
|
`Trust.Revocation
|
|
]
|
|
|
|
lean_lib Build where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Build.Coeffect,
|
|
`Build.Attestation,
|
|
`Build.Ecosystem,
|
|
`Build.Reproducibility
|
|
]
|
|
|
|
lean_lib Compute where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Compute.CrossChain
|
|
]
|
|
|
|
lean_lib DeFi where
|
|
srcDir := "."
|
|
roots := #[
|
|
`DeFi.OrderBook,
|
|
`DeFi.AMM,
|
|
`DeFi.HFT,
|
|
`DeFi.FeeModel,
|
|
`DeFi.LiquidStaking,
|
|
`DeFi.Router,
|
|
`DeFi.FlashLoan,
|
|
`DeFi.Governance
|
|
]
|
|
|
|
lean_lib Network where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Network.PeerDiscovery
|
|
]
|
|
|
|
lean_lib Bridge where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Bridge.Teleport
|
|
]
|
|
|
|
require mathlib from git
|
|
"https://github.com/leanprover-community/mathlib4" @ "v4.14.0"
|